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

Theorem com14 85
Description: Commutation of antecedents. Swap 1st and 4th. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
com14  |-  ( th 
->  ( ps  ->  ( ch  ->  ( ph  ->  ta ) ) ) )

Proof of Theorem com14
StepHypRef Expression
1 com4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21com4l 81 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
32com3r 76 1  |-  ( th 
->  ( ps  ->  ( ch  ->  ( ph  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  f1o2ndf1  6455  fiint  7384  dfac5  8010  ltexprlem7  8920  rpnnen1lem5  10605  difreicc  11029  elfznelfzo  11193  injresinjlem  11200  brfi1uzind  11716  infpnlem1  13279  neindisj2  17188  alexsubALTlem3  18081  nbcusgra  21473  cusgrares  21482  cusgrasize2inds  21487  uvtxnbgra  21503  1pthoncl  21593  wlkdvspthlem  21608  wlkdvspth  21609  usgrcyclnl1  21628  3v3e3cycl1  21632  4cycl4v4e  21654  4cycl4dv4e  21656  zerdivemp1  22023  spansncvi  23155  cdj3lem2b  23941  predpo  25460  wfrlem12  25550  frrlem11  25595  zerdivemp1x  26572  funbrafv  27999  ssfz12  28105  fz0fzdiffz0  28120  ubmelfzo  28127  ubmelm1fzo  28128  ssfzo12  28131  swrd0swrd  28198  swrdswrd  28200  2cshw1lem2  28250  cshweqdif2s  28272  usgra2pthlem1  28311  el2wlkonot  28337  usg2wlkonot  28351  usg2wotspth  28352  2pthfrgra  28402  3cyclfrgrarn1  28403  frgranbnb  28411  vdgn0frgrav2  28416  frgrancvvdeqlemC  28429  frg2woteq  28450  usg2spot2nb  28455  ee233  28603
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator