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

Theorem com14 96
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 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
com14 (𝜃 → (𝜓 → (𝜒 → (𝜑𝜏))))

Proof of Theorem com14
StepHypRef Expression
1 com4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21com4l 92 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
32com3r 87 1 (𝜃 → (𝜓 → (𝜒 → (𝜑𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  propeqop  5389  iunopeqop  5403  predpo  6160  fveqdmss  6839  f1o2ndf1  7809  wfrlem12  7957  fiint  8784  dfac5  9543  ltexprlem7  10453  rpnnen1lem5  12370  fz0fzdiffz0  13006  elfzodifsumelfzo  13093  ssfzo12  13120  elfznelfzo  13132  injresinjlem  13147  addmodlteq  13304  suppssfz  13352  fi1uzind  13845  swrdswrd  14057  cshf1  14162  s3iunsndisj  14318  dfgcd2  15884  cncongr1  16001  infpnlem1  16236  prmgaplem6  16382  initoeu1  17261  termoeu1  17268  cply1mul  20392  pm2mpf1  21337  mp2pm2mplem4  21347  neindisj2  21661  alexsubALTlem3  22587  2sqreultlem  25951  2sqreunnltlem  25954  nbuhgr2vtx1edgblem  27061  cusgrsize2inds  27163  2pthnloop  27440  upgrwlkdvdelem  27445  usgr2pthlem  27472  wwlksnextbi  27600  wspn0  27631  rusgrnumwwlks  27681  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwwlkf  27754  clwwlknonex2lem2  27815  uhgr3cyclexlem  27888  3cyclfrgrrn1  27992  frgrnbnb  28000  frgrncvvdeqlem9  28014  frgrwopreglem2  28020  frgrregord013  28102  friendship  28106  spansncvi  29357  cdj3lem2b  30142  sat1el2xp  32524  bj-cbvalim  33876  bj-cbvexim  33877  zerdivemp1x  35108  ee233  40733  funbrafv  43238  ssfz12  43395  iccpartnel  43445  poprelb  43533  lighneal  43623  tgoldbach  43829  isomuspgrlem2d  43843  lidldomn1  44090  rngccatidALTV  44158  ringccatidALTV  44221  ply1mulgsumlem1  44338  lindslinindsimp2  44416  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator