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  5454  iunopeqop  5468  fveqdmss  7016  f1o2ndf1  8062  fiint  9235  fiintOLD  9236  dfac5  10042  ltexprlem7  10955  rpnnen1lem5  12900  fz0fzdiffz0  13558  elfzodifsumelfzo  13652  ssfzo12  13680  elfznelfzo  13693  injresinjlem  13708  addmodlteq  13871  suppssfz  13919  fi1uzind  14432  swrdswrd  14629  cshf1  14734  s3iunsndisj  14893  dfgcd2  16475  cncongr1  16596  infpnlem1  16840  prmgaplem6  16986  initoeu1  17936  termoeu1  17943  cply1mul  22199  pm2mpf1  22702  mp2pm2mplem4  22712  neindisj2  23026  alexsubALTlem3  23952  2sqreultlem  27374  2sqreunnltlem  27377  nbuhgr2vtx1edgblem  29314  cusgrsize2inds  29417  2pthnloop  29694  upgrwlkdvdelem  29699  usgr2pthlem  29726  cyclnumvtx  29763  wwlksnextbi  29857  wspn0  29887  rusgrnumwwlks  29937  clwlkclwwlklem2a  29960  clwlkclwwlklem2  29962  clwwlkf  30009  clwwlknonex2lem2  30070  uhgr3cyclexlem  30143  3cyclfrgrrn1  30247  frgrnbnb  30255  frgrncvvdeqlem9  30269  frgrwopreglem2  30275  frgrregord013  30357  friendship  30361  spansncvi  31614  cdj3lem2b  32399  sat1el2xp  35351  bj-cbvalim  36618  bj-cbvexim  36619  zerdivemp1x  37926  ee233  44493  funbrafv  47143  ssfz12  47299  iccpartnel  47423  poprelb  47509  lighneal  47596  tgoldbach  47802  clnbgrgrim  47919  lidldomn1  48216  rngccatidALTV  48257  ringccatidALTV  48291  ply1mulgsumlem1  48372  lindslinindsimp2  48449  nn0sumshdiglemA  48605  nn0sumshdiglemB  48606