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  7133  dfac5  7755  ltexprlem7  8666  rpnnen1lem5  10346  difreicc  10767  infpnlem1  12957  neindisj2  16860  alexsubALTlem3  17743  spansncvi  22231  cdj3lem2b  23017  predpo  24184  wfrlem12  24267  frrlem11  24293  eqfnung2  25118  oriso  25214  zerdivemp1  25436  svs2  25487  lvsovso  25626  cmpmon  25815  icmpmon  25816  inttaror  25900  isconcl5a  26101  isconcl5ab  26102  bsstr  26128  nbssntr  26129  lppotos  26144  pdiveql  26168  zerdivemp1x  26586  funbrafv  28020  nbcusgra  28159  uvtxnbgra  28165  ee233  28281
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator