Theorem com14 97

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 93	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	com3r 88	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  5480  iunopeqop  5494  iunopeqopOLD  5495  fveqdmss  7063  f1o2ndf1  8105  fiint  9274  dfac5  10100  ltexprlem7  11015  rpnnen1lem5  12993  fz0fzdiffz0  13653  elfzodifsumelfzo  13748  ssfzo12  13776  elfznelfzo  13790  injresinjlem  13807  addmodlteq  13970  suppssfz  14018  fi1uzind  14532  swrdswrd  14730  cshf1  14835  s3iunsndisj  14993  dfgcd2  16592  cncongr1  16713  infpnlem1  16958  prmgaplem6  17104  initoeu1  18056  termoeu1  18063  cply1mul  22413  pm2mpf1  22913  mp2pm2mplem4  22923  neindisj2  23237  alexsubALTlem3  24163  2sqreultlem  27565  2sqreunnltlem  27568  nbuhgr2vtx1edgblem  29606  cusgrsize2inds  29708  2pthnloop  29985  upgrwlkdvdelem  29990  usgr2pthlem  30017  cyclnumvtx  30054  wwlksnextbi  30148  wspn0  30178  rusgrnumwwlks  30231  clwlkclwwlklem2a  30254  clwlkclwwlklem2  30256  clwwlkf  30303  clwwlknonex2lem2  30364  uhgr3cyclexlem  30437  3cyclfrgrrn1  30541  frgrnbnb  30549  frgrncvvdeqlem9  30563  frgrwopreglem2  30569  frgrregord013  30651  friendship  30655  spansncvi  31909  cdj3lem2b  32694  sat1el2xp  35737  zerdivemp1x  38453  ee233  45087  funbrafv  47751  ssfz12  47907  nnmul2b  47924  iccpartnel  48043  poprelb  48129  lighneal  48219  tgoldbach  48438  clnbgrgrim  48555  lidldomn1  48852  rngccatidALTV  48893  ringccatidALTV  48927  ply1mulgsumlem1  49018  lindslinindsimp2  49095  nn0sumshdiglemA  49251  nn0sumshdiglemB  49252