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  6593  nndi  6637  nnmass  6638  ttukeylem5  8156  genpnmax  8647  mulexp  11157  expadd  11160  expmul  11163  grpomndo  21029  5oalem6  22254  atom1d  22949  claddrvr  25751  sigadd  25752  clscnc  26113  pell14qrexpclnn0  27054  truniALT  28604  truniALTVD  28970
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