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

Theorem exp3acom3r 1379
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 426 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com3l 77 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  odi  6822  nndi  6866  nnmass  6867  ttukeylem5  8393  genpnmax  8884  mulexp  11419  expadd  11422  expmul  11425  usgraidx2vlem2  21411  grpomndo  21934  5oalem6  23161  atom1d  23856  pell14qrexpclnn0  26929  usg2wlkonot  28350  usg2spot2nb  28454  truniALT  28626  truniALTVD  28990
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 178  df-an 361
  Copyright terms: Public domain W3C validator