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  5465  iunopeqop  5479  fveqdmss  7030  f1o2ndf1  8055  wfrlem12OLD  8267  fiint  9271  dfac5  10069  ltexprlem7  10983  rpnnen1lem5  12911  fz0fzdiffz0  13556  elfzodifsumelfzo  13644  ssfzo12  13671  elfznelfzo  13683  injresinjlem  13698  addmodlteq  13857  suppssfz  13905  fi1uzind  14402  swrdswrd  14599  cshf1  14704  s3iunsndisj  14859  dfgcd2  16432  cncongr1  16548  infpnlem1  16787  prmgaplem6  16933  initoeu1  17902  termoeu1  17909  cply1mul  21681  pm2mpf1  22164  mp2pm2mplem4  22174  neindisj2  22490  alexsubALTlem3  23416  2sqreultlem  26811  2sqreunnltlem  26814  nbuhgr2vtx1edgblem  28341  cusgrsize2inds  28443  2pthnloop  28721  upgrwlkdvdelem  28726  usgr2pthlem  28753  wwlksnextbi  28881  wspn0  28911  rusgrnumwwlks  28961  clwlkclwwlklem2a  28984  clwlkclwwlklem2  28986  clwwlkf  29033  clwwlknonex2lem2  29094  uhgr3cyclexlem  29167  3cyclfrgrrn1  29271  frgrnbnb  29279  frgrncvvdeqlem9  29293  frgrwopreglem2  29299  frgrregord013  29381  friendship  29385  spansncvi  30636  cdj3lem2b  31421  sat1el2xp  34030  bj-cbvalim  35155  bj-cbvexim  35156  zerdivemp1x  36452  ee233  42889  funbrafv  45476  ssfz12  45632  iccpartnel  45716  poprelb  45802  lighneal  45889  tgoldbach  46095  isomuspgrlem2d  46109  lidldomn1  46305  rngccatidALTV  46373  ringccatidALTV  46436  ply1mulgsumlem1  46553  lindslinindsimp2  46630  nn0sumshdiglemA  46791  nn0sumshdiglemB  46792
  Copyright terms: Public domain W3C validator