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  5461  iunopeqop  5475  iunopeqopOLD  5476  fveqdmss  7030  f1o2ndf1  8072  fiint  9237  dfac5  10051  ltexprlem7  10965  rpnnen1lem5  12931  fz0fzdiffz0  13591  elfzodifsumelfzo  13686  ssfzo12  13714  elfznelfzo  13728  injresinjlem  13745  addmodlteq  13908  suppssfz  13956  fi1uzind  14469  swrdswrd  14667  cshf1  14772  s3iunsndisj  14930  dfgcd2  16515  cncongr1  16636  infpnlem1  16881  prmgaplem6  17027  initoeu1  17978  termoeu1  17985  cply1mul  22261  pm2mpf1  22764  mp2pm2mplem4  22774  neindisj2  23088  alexsubALTlem3  24014  2sqreultlem  27410  2sqreunnltlem  27413  nbuhgr2vtx1edgblem  29420  cusgrsize2inds  29522  2pthnloop  29799  upgrwlkdvdelem  29804  usgr2pthlem  29831  cyclnumvtx  29868  wwlksnextbi  29962  wspn0  29992  rusgrnumwwlks  30045  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwwlkf  30117  clwwlknonex2lem2  30178  uhgr3cyclexlem  30251  3cyclfrgrrn1  30355  frgrnbnb  30363  frgrncvvdeqlem9  30377  frgrwopreglem2  30383  frgrregord013  30465  friendship  30469  spansncvi  31723  cdj3lem2b  32508  sat1el2xp  35561  zerdivemp1x  38268  ee233  44946  funbrafv  47606  ssfz12  47762  nnmul2b  47779  iccpartnel  47898  poprelb  47984  lighneal  48074  tgoldbach  48293  clnbgrgrim  48410  lidldomn1  48707  rngccatidALTV  48748  ringccatidALTV  48782  ply1mulgsumlem1  48862  lindslinindsimp2  48939  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096