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

Theorem exp3acom23 1362
Description: The exportation deduction exp3a 425 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 425 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 72 1  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  simplbi2comg  1363  ax10  1884  reupick  3452  trintss  4129  pwssun  4299  ordelord  4414  tz7.7  4418  poxp  6227  smores2  6371  smoiun  6378  smogt  6384  tz7.49  6457  abianfp  6471  omsmolem  6651  mapxpen  7027  suplub2  7212  epfrs  7413  r1sdom  7446  rankr1ai  7470  ficardom  7594  cardsdomel  7607  dfac5lem5  7754  cfsmolem  7896  cfcoflem  7898  axdc3lem2  8077  zorn2lem7  8129  genpn0  8627  reclem2pr  8672  supsrlem  8733  ltletr  8913  rpneg  10383  xrltletr  10488  iccid  10701  o1rlimmul  12092  divalgb  12603  bezoutlem3  12719  lss1d  15720  txlm  17342  fmfnfmlem1  17649  blsscls2  18050  metcnpi3  18092  pf1ind  19438  bcmono  20516  ocnel  21877  atcvat2i  22967  atcvat4i  22977  dfon2lem5  24143  cgrxfr  24678  colinearxfr  24698  hfelhf  24811  tartarmap  25888  fnctartar  25907  seqpo  26457  nbusgra  28143  onfrALTlem2  28311  onfrALTlem2VD  28665  atlatle  29510  cvrexchlem  29608  cvrat2  29618  cvrat4  29632  pmapjoin  30041
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