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

Theorem com14 82
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 78 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
32com3r 73 1  |-  ( th 
->  ( ps  ->  ( ch  ->  ( ph  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  fiint  7178  dfac5  7800  ltexprlem7  8711  rpnnen1lem5  10393  difreicc  10814  infpnlem1  13004  neindisj2  16916  alexsubALTlem3  17795  zerdivemp1  21154  spansncvi  22286  cdj3lem2b  23072  predpo  24569  wfrlem12  24652  frrlem11  24678  zerdivemp1x  25734  funbrafv  27171  elfznelfzo  27275  injresinjlem  27276  nbcusgra  27408  uvtxnbgra  27416  1pthoncl  27488  wlkdvspthlem  27503  wlkdvspth  27504  usgrcyclnl1  27524  3v3e3cycl1  27528  4cycl4v4e  27550  4cycl4dv4e  27552  2pthfrgra  27603  3cyclfrgrarn1  27604  frgranbnb  27612  vdgn0frgrav2  27617  frgrancvvdeqlemC  27631  ee233  27775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator