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  7024  f1o2ndf1  8065  fiint  9230  dfac5  10042  ltexprlem7  10956  rpnnen1lem5  12922  fz0fzdiffz0  13582  elfzodifsumelfzo  13677  ssfzo12  13705  elfznelfzo  13719  injresinjlem  13736  addmodlteq  13899  suppssfz  13947  fi1uzind  14460  swrdswrd  14658  cshf1  14763  s3iunsndisj  14921  dfgcd2  16506  cncongr1  16627  infpnlem1  16872  prmgaplem6  17018  initoeu1  17969  termoeu1  17976  cply1mul  22271  pm2mpf1  22774  mp2pm2mplem4  22784  neindisj2  23098  alexsubALTlem3  24024  2sqreultlem  27424  2sqreunnltlem  27427  nbuhgr2vtx1edgblem  29434  cusgrsize2inds  29537  2pthnloop  29814  upgrwlkdvdelem  29819  usgr2pthlem  29846  cyclnumvtx  29883  wwlksnextbi  29977  wspn0  30007  rusgrnumwwlks  30060  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  clwwlkf  30132  clwwlknonex2lem2  30193  uhgr3cyclexlem  30266  3cyclfrgrrn1  30370  frgrnbnb  30378  frgrncvvdeqlem9  30392  frgrwopreglem2  30398  frgrregord013  30480  friendship  30484  spansncvi  31738  cdj3lem2b  32523  sat1el2xp  35577  zerdivemp1x  38282  ee233  44964  funbrafv  47618  ssfz12  47774  nnmul2b  47791  iccpartnel  47910  poprelb  47996  lighneal  48086  tgoldbach  48305  clnbgrgrim  48422  lidldomn1  48719  rngccatidALTV  48760  ringccatidALTV  48794  ply1mulgsumlem1  48874  lindslinindsimp2  48951  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108