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

Theorem com14 84
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 80 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
32com3r 75 1  |-  ( th 
->  ( ps  ->  ( ch  ->  ( ph  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  f1o2ndf1  6413  fiint  7342  dfac5  7965  ltexprlem7  8875  rpnnen1lem5  10560  difreicc  10984  elfznelfzo  11147  injresinjlem  11154  brfi1uzind  11670  infpnlem1  13233  neindisj2  17142  alexsubALTlem3  18033  nbcusgra  21425  cusgrares  21434  cusgrasize2inds  21439  uvtxnbgra  21455  1pthoncl  21545  wlkdvspthlem  21560  wlkdvspth  21561  usgrcyclnl1  21580  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  zerdivemp1  21975  spansncvi  23107  cdj3lem2b  23893  predpo  25398  wfrlem12  25481  frrlem11  25507  zerdivemp1x  26461  funbrafv  27889  ssfz12  27976  ubmelfzo  27986  ubmelm1fzo  27987  ssfzo12  27990  swrd0swrd  28009  swrdswrd  28011  swrdccat3b  28031  usgra2pthlem1  28040  el2wlkonot  28066  usg2wlkonot  28080  usg2wotspth  28081  2pthfrgra  28115  3cyclfrgrarn1  28116  frgranbnb  28124  vdgn0frgrav2  28129  frgrancvvdeqlemC  28142  frg2woteq  28163  usg2spot2nb  28168  ee233  28313
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator