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  5467  iunopeqop  5481  fveqdmss  7050  f1o2ndf1  8101  fiint  9277  fiintOLD  9278  dfac5  10082  ltexprlem7  10995  rpnnen1lem5  12940  fz0fzdiffz0  13598  elfzodifsumelfzo  13692  ssfzo12  13720  elfznelfzo  13733  injresinjlem  13748  addmodlteq  13911  suppssfz  13959  fi1uzind  14472  swrdswrd  14670  cshf1  14775  s3iunsndisj  14934  dfgcd2  16516  cncongr1  16637  infpnlem1  16881  prmgaplem6  17027  initoeu1  17973  termoeu1  17980  cply1mul  22183  pm2mpf1  22686  mp2pm2mplem4  22696  neindisj2  23010  alexsubALTlem3  23936  2sqreultlem  27358  2sqreunnltlem  27361  nbuhgr2vtx1edgblem  29278  cusgrsize2inds  29381  2pthnloop  29661  upgrwlkdvdelem  29666  usgr2pthlem  29693  cyclnumvtx  29730  wwlksnextbi  29824  wspn0  29854  rusgrnumwwlks  29904  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwwlkf  29976  clwwlknonex2lem2  30037  uhgr3cyclexlem  30110  3cyclfrgrrn1  30214  frgrnbnb  30222  frgrncvvdeqlem9  30236  frgrwopreglem2  30242  frgrregord013  30324  friendship  30328  spansncvi  31581  cdj3lem2b  32366  sat1el2xp  35366  bj-cbvalim  36633  bj-cbvexim  36634  zerdivemp1x  37941  ee233  44509  funbrafv  47156  ssfz12  47312  iccpartnel  47436  poprelb  47522  lighneal  47609  tgoldbach  47815  clnbgrgrim  47931  lidldomn1  48216  rngccatidALTV  48257  ringccatidALTV  48291  ply1mulgsumlem1  48372  lindslinindsimp2  48449  nn0sumshdiglemA  48605  nn0sumshdiglemB  48606