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

Theorem exp3acom23 1378
Description: The exportation deduction exp3a 426 with commutation of the conjoined wwfs. (Contributed by Alan Sare, 22-Jul-2012.)
Hypothesis
Ref Expression
exp3acom23.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
exp3acom23  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )

Proof of Theorem exp3acom23
StepHypRef Expression
1 exp3acom23.1 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21exp3a 426 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 74 1  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simplbi2comg  1379  ax10  1976  reupick  3561  trintss  4252  pwssun  4423  ordelord  4537  tz7.7  4541  poxp  6387  smores2  6545  smoiun  6552  smogt  6558  tz7.49  6631  abianfp  6645  omsmolem  6825  mapxpen  7202  suplub2  7392  epfrs  7593  r1sdom  7626  rankr1ai  7650  ficardom  7774  cardsdomel  7787  dfac5lem5  7934  cfsmolem  8076  cfcoflem  8078  axdc3lem2  8257  zorn2lem7  8308  genpn0  8806  reclem2pr  8851  supsrlem  8912  ltletr  9092  rpneg  10566  xrltletr  10672  iccid  10886  o1rlimmul  12332  divalgb  12844  bezoutlem3  12960  lss1d  15959  txlm  17594  fmfnfmlem1  17900  blsscls2  18417  metcnpi3  18459  pf1ind  19835  bcmono  20921  nbusgra  21299  redwlk  21447  ocnel  22641  atcvat2i  23731  atcvat4i  23741  dfon2lem5  25160  cgrxfr  25696  colinearxfr  25716  hfelhf  25829  seqpo  26135  onfrALTlem2  27968  onfrALTlem2VD  28335  ax10NEW7  28804  atlatle  29486  cvrexchlem  29584  cvrat2  29594  cvrat4  29608  pmapjoin  30017
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