MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp3acom3r Unicode version

Theorem exp3acom3r 1360
Description: Export and commute antecedents. (Contributed by Alan Sare, 18-Mar-2012.)
Hypothesis
Ref Expression
exp3acom3r.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
exp3acom3r  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )

Proof of Theorem exp3acom3r
StepHypRef Expression
1 exp3acom3r.1 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21exp3a 425 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com3l 75 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  odi  6577  nndi  6621  nnmass  6622  ttukeylem5  8140  genpnmax  8631  mulexp  11141  expadd  11144  expmul  11147  grpomndo  21013  5oalem6  22238  atom1d  22933  claddrvr  25060  sigadd  25061  clscnc  25422  pell14qrexpclnn0  26363  truniALT  27678  truniALTVD  28027
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator