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

Step	Hyp	Ref	Expression
1		com4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com4l 92	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	com3r 87	1 ⊢ (𝜃 → (𝜓 → (𝜒 → (𝜑 → 𝜏))))

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  5526  iunopeqop  5540  fveqdmss  7112  f1o2ndf1  8163  wfrlem12OLD  8376  fiint  9394  fiintOLD  9395  dfac5  10198  ltexprlem7  11111  rpnnen1lem5  13046  fz0fzdiffz0  13694  elfzodifsumelfzo  13782  ssfzo12  13809  elfznelfzo  13822  injresinjlem  13837  addmodlteq  13997  suppssfz  14045  fi1uzind  14556  swrdswrd  14753  cshf1  14858  s3iunsndisj  15017  dfgcd2  16593  cncongr1  16714  infpnlem1  16957  prmgaplem6  17103  initoeu1  18078  termoeu1  18085  cply1mul  22321  pm2mpf1  22826  mp2pm2mplem4  22836  neindisj2  23152  alexsubALTlem3  24078  2sqreultlem  27509  2sqreunnltlem  27512  nbuhgr2vtx1edgblem  29386  cusgrsize2inds  29489  2pthnloop  29767  upgrwlkdvdelem  29772  usgr2pthlem  29799  wwlksnextbi  29927  wspn0  29957  rusgrnumwwlks  30007  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwwlkf  30079  clwwlknonex2lem2  30140  uhgr3cyclexlem  30213  3cyclfrgrrn1  30317  frgrnbnb  30325  frgrncvvdeqlem9  30339  frgrwopreglem2  30345  frgrregord013  30427  friendship  30431  spansncvi  31684  cdj3lem2b  32469  sat1el2xp  35347  bj-cbvalim  36611  bj-cbvexim  36612  zerdivemp1x  37907  ee233  44490  funbrafv  47073  ssfz12  47229  iccpartnel  47312  poprelb  47398  lighneal  47485  tgoldbach  47691  clnbgrgrim  47786  lidldomn1  47954  rngccatidALTV  47995  ringccatidALTV  48029  ply1mulgsumlem1  48115  lindslinindsimp2  48192  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354