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  5455  iunopeqop  5469  fveqdmss  7023  f1o2ndf1  8064  fiint  9227  dfac5  10039  ltexprlem7  10953  rpnnen1lem5  12894  fz0fzdiffz0  13553  elfzodifsumelfzo  13647  ssfzo12  13675  elfznelfzo  13689  injresinjlem  13706  addmodlteq  13869  suppssfz  13917  fi1uzind  14430  swrdswrd  14628  cshf1  14733  s3iunsndisj  14891  dfgcd2  16473  cncongr1  16594  infpnlem1  16838  prmgaplem6  16984  initoeu1  17935  termoeu1  17942  cply1mul  22240  pm2mpf1  22743  mp2pm2mplem4  22753  neindisj2  23067  alexsubALTlem3  23993  2sqreultlem  27414  2sqreunnltlem  27417  nbuhgr2vtx1edgblem  29424  cusgrsize2inds  29527  2pthnloop  29804  upgrwlkdvdelem  29809  usgr2pthlem  29836  cyclnumvtx  29873  wwlksnextbi  29967  wspn0  29997  rusgrnumwwlks  30050  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwwlkf  30122  clwwlknonex2lem2  30183  uhgr3cyclexlem  30256  3cyclfrgrrn1  30360  frgrnbnb  30368  frgrncvvdeqlem9  30382  frgrwopreglem2  30388  frgrregord013  30470  friendship  30474  spansncvi  31727  cdj3lem2b  32512  sat1el2xp  35573  bj-cbvalim  36845  bj-cbvexim  36846  zerdivemp1x  38148  ee233  44760  funbrafv  47404  ssfz12  47560  iccpartnel  47684  poprelb  47770  lighneal  47857  tgoldbach  48063  clnbgrgrim  48180  lidldomn1  48477  rngccatidALTV  48518  ringccatidALTV  48552  ply1mulgsumlem1  48632  lindslinindsimp2  48709  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866