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  5511  iunopeqop  5525  fveqdmss  7097  f1o2ndf1  8148  wfrlem12OLD  8361  fiint  9367  fiintOLD  9368  dfac5  10170  ltexprlem7  11083  rpnnen1lem5  13024  fz0fzdiffz0  13678  elfzodifsumelfzo  13771  ssfzo12  13799  elfznelfzo  13812  injresinjlem  13827  addmodlteq  13988  suppssfz  14036  fi1uzind  14547  swrdswrd  14744  cshf1  14849  s3iunsndisj  15008  dfgcd2  16584  cncongr1  16705  infpnlem1  16949  prmgaplem6  17095  initoeu1  18057  termoeu1  18064  cply1mul  22301  pm2mpf1  22806  mp2pm2mplem4  22816  neindisj2  23132  alexsubALTlem3  24058  2sqreultlem  27492  2sqreunnltlem  27495  nbuhgr2vtx1edgblem  29369  cusgrsize2inds  29472  2pthnloop  29752  upgrwlkdvdelem  29757  usgr2pthlem  29784  cyclnumvtx  29821  wwlksnextbi  29915  wspn0  29945  rusgrnumwwlks  29995  clwlkclwwlklem2a  30018  clwlkclwwlklem2  30020  clwwlkf  30067  clwwlknonex2lem2  30128  uhgr3cyclexlem  30201  3cyclfrgrrn1  30305  frgrnbnb  30313  frgrncvvdeqlem9  30327  frgrwopreglem2  30333  frgrregord013  30415  friendship  30419  spansncvi  31672  cdj3lem2b  32457  sat1el2xp  35385  bj-cbvalim  36647  bj-cbvexim  36648  zerdivemp1x  37955  ee233  44544  funbrafv  47175  ssfz12  47331  iccpartnel  47430  poprelb  47516  lighneal  47603  tgoldbach  47809  clnbgrgrim  47907  lidldomn1  48152  rngccatidALTV  48193  ringccatidALTV  48227  ply1mulgsumlem1  48308  lindslinindsimp2  48385  nn0sumshdiglemA  48545  nn0sumshdiglemB  48546