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

Theorem exp3acom23 1381
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  1382  ax10OLD  2032  reupick  3617  trintss  4310  pwssun  4481  ordelord  4595  tz7.7  4599  poxp  6450  smores2  6608  smoiun  6615  smogt  6621  tz7.49  6694  abianfp  6708  omsmolem  6888  mapxpen  7265  suplub2  7456  epfrs  7657  r1sdom  7690  rankr1ai  7714  ficardom  7838  cardsdomel  7851  dfac5lem5  7998  cfsmolem  8140  cfcoflem  8142  axdc3lem2  8321  zorn2lem7  8372  genpn0  8870  reclem2pr  8915  supsrlem  8976  ltletr  9156  rpneg  10631  xrltletr  10737  iccid  10951  o1rlimmul  12402  divalgb  12914  bezoutlem3  13030  lss1d  16029  txlm  17670  fmfnfmlem1  17976  blsscls2  18524  metcnpi3  18566  pf1ind  19965  bcmono  21051  nbusgra  21430  redwlk  21596  ocnel  22790  atcvat2i  23880  atcvat4i  23890  dfon2lem5  25402  cgrxfr  25954  colinearxfr  25974  hfelhf  26087  seqpo  26405  elfz2z  28053  ccatsymb  28116  swrdvalodmlem1  28123  swrdccatin12lem3  28142  cshweqdif2s  28198  usg2spot2nb  28355  onfrALTlem2  28533  onfrALTlem2VD  28902  ax10NEW7  29374  atlatle  30019  cvrexchlem  30117  cvrat2  30127  cvrat4  30141  pmapjoin  30550
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