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

Theorem exp3acom3r 1419
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 436 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com3l 81 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  odi  7008  nndi  7052  nnmass  7053  ttukeylem5  8672  genpnmax  9166  mulexp  11889  expadd  11892  expmul  11895  usgraidx2vlem2  23135  grpomndo  23658  5oalem6  24887  atom1d  25582  pell14qrexpclnn0  29054  usg2wlkonot  30250  clwwlkel  30303  clwwlkf1  30306  erclwwlktr  30333  erclwwlkntr  30349  usg2spot2nb  30506  truniALT  30989  truniALTVD  31356
  Copyright terms: Public domain W3C validator