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  5450  iunopeqop  5464  fveqdmss  7017  f1o2ndf1  8058  fiint  9218  dfac5  10027  ltexprlem7  10940  rpnnen1lem5  12881  fz0fzdiffz0  13539  elfzodifsumelfzo  13633  ssfzo12  13661  elfznelfzo  13675  injresinjlem  13692  addmodlteq  13855  suppssfz  13903  fi1uzind  14416  swrdswrd  14614  cshf1  14719  s3iunsndisj  14877  dfgcd2  16459  cncongr1  16580  infpnlem1  16824  prmgaplem6  16970  initoeu1  17920  termoeu1  17927  cply1mul  22212  pm2mpf1  22715  mp2pm2mplem4  22725  neindisj2  23039  alexsubALTlem3  23965  2sqreultlem  27386  2sqreunnltlem  27389  nbuhgr2vtx1edgblem  29331  cusgrsize2inds  29434  2pthnloop  29711  upgrwlkdvdelem  29716  usgr2pthlem  29743  cyclnumvtx  29780  wwlksnextbi  29874  wspn0  29904  rusgrnumwwlks  29957  clwlkclwwlklem2a  29980  clwlkclwwlklem2  29982  clwwlkf  30029  clwwlknonex2lem2  30090  uhgr3cyclexlem  30163  3cyclfrgrrn1  30267  frgrnbnb  30275  frgrncvvdeqlem9  30289  frgrwopreglem2  30295  frgrregord013  30377  friendship  30381  spansncvi  31634  cdj3lem2b  32419  sat1el2xp  35444  bj-cbvalim  36710  bj-cbvexim  36711  zerdivemp1x  38008  ee233  44637  funbrafv  47283  ssfz12  47439  iccpartnel  47563  poprelb  47649  lighneal  47736  tgoldbach  47942  clnbgrgrim  48059  lidldomn1  48356  rngccatidALTV  48397  ringccatidALTV  48431  ply1mulgsumlem1  48512  lindslinindsimp2  48589  nn0sumshdiglemA  48745  nn0sumshdiglemB  48746