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  5463  iunopeqop  5477  fveqdmss  7032  f1o2ndf1  8074  fiint  9239  dfac5  10051  ltexprlem7  10965  rpnnen1lem5  12906  fz0fzdiffz0  13565  elfzodifsumelfzo  13659  ssfzo12  13687  elfznelfzo  13701  injresinjlem  13718  addmodlteq  13881  suppssfz  13929  fi1uzind  14442  swrdswrd  14640  cshf1  14745  s3iunsndisj  14903  dfgcd2  16485  cncongr1  16606  infpnlem1  16850  prmgaplem6  16996  initoeu1  17947  termoeu1  17954  cply1mul  22252  pm2mpf1  22755  mp2pm2mplem4  22765  neindisj2  23079  alexsubALTlem3  24005  2sqreultlem  27426  2sqreunnltlem  27429  nbuhgr2vtx1edgblem  29436  cusgrsize2inds  29539  2pthnloop  29816  upgrwlkdvdelem  29821  usgr2pthlem  29848  cyclnumvtx  29885  wwlksnextbi  29979  wspn0  30009  rusgrnumwwlks  30062  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwwlkf  30134  clwwlknonex2lem2  30195  uhgr3cyclexlem  30268  3cyclfrgrrn1  30372  frgrnbnb  30380  frgrncvvdeqlem9  30394  frgrwopreglem2  30400  frgrregord013  30482  friendship  30486  spansncvi  31739  cdj3lem2b  32524  sat1el2xp  35592  bj-cbvalim  36886  bj-cbvexim  36887  zerdivemp1x  38195  ee233  44872  funbrafv  47515  ssfz12  47671  iccpartnel  47795  poprelb  47881  lighneal  47968  tgoldbach  48174  clnbgrgrim  48291  lidldomn1  48588  rngccatidALTV  48629  ringccatidALTV  48663  ply1mulgsumlem1  48743  lindslinindsimp2  48820  nn0sumshdiglemA  48976  nn0sumshdiglemB  48977