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  1897  reupick  3465  trintss  4145  pwssun  4315  ordelord  4430  tz7.7  4434  poxp  6243  smores2  6387  smoiun  6394  smogt  6400  tz7.49  6473  abianfp  6487  omsmolem  6667  mapxpen  7043  suplub2  7228  epfrs  7429  r1sdom  7462  rankr1ai  7486  ficardom  7610  cardsdomel  7623  dfac5lem5  7770  cfsmolem  7912  cfcoflem  7914  axdc3lem2  8093  zorn2lem7  8145  genpn0  8643  reclem2pr  8688  supsrlem  8749  ltletr  8929  rpneg  10399  xrltletr  10504  iccid  10717  o1rlimmul  12108  divalgb  12619  bezoutlem3  12735  lss1d  15736  txlm  17358  fmfnfmlem1  17665  blsscls2  18066  metcnpi3  18108  pf1ind  19454  bcmono  20532  ocnel  21893  atcvat2i  22983  atcvat4i  22993  dfon2lem5  24214  cgrxfr  24750  colinearxfr  24770  hfelhf  24883  tartarmap  25991  fnctartar  26010  seqpo  26560  nbusgra  28277  redwlk  28364  onfrALTlem2  28610  onfrALTlem2VD  28981  ax10NEW7  29450  atlatle  30132  cvrexchlem  30230  cvrat2  30240  cvrat4  30254  pmapjoin  30663
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