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 ⊢ (𝜃 → (𝜓 → (𝜒 → (𝜑 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  propeqop  5478  iunopeqop  5493  iunopeqopOLD  5494  fveqdmss  7079  f1o2ndf1  8136  fiint  9322  dfac5  10211  ltexprlem7  11131  rpnnen1lem5  13113  fz0fzdiffz0  13775  elfzodifsumelfzo  13870  ssfzo12  13898  elfznelfzo  13912  injresinjlem  13929  addmodlteq  14093  suppssfz  14141  fi1uzind  14656  swrdswrd  14859  cshf1  14966  s3iunsndisj  15127  dfgcd2  16725  cncongr1  16848  infpnlem1  17094  prmgaplem6  17240  initoeu1  18192  termoeu1  18199  cply1mul  22620  pm2mpf1  23123  mp2pm2mplem4  23133  neindisj2  23447  alexsubALTlem3  24374  2sqreultlem  27780  2sqreunnltlem  27783  nbuhgr2vtx1edgblem  29938  cusgrsize2inds  30040  2pthnloop  30323  upgrwlkdvdelem  30328  usgr2pthlem  30355  cyclnumvtx  30394  wwlksnextbi  30489  wspn0  30519  rusgrnumwwlks  30572  clwlkclwwlklem2a  30595  clwlkclwwlklem2  30597  clwwlkf  30644  clwwlknonex2lem2  30705  uhgr3cyclexlem  30788  3cyclfrgrrn1  30892  frgrnbnb  30900  frgrncvvdeqlem9  30914  frgrwopreglem2  30920  frgrregord013  31002  friendship  31006  spansncvi  32260  cdj3lem2b  33045  sat1el2xp  36231  zerdivemp1x  38975  ee233  45596  funbrafv  48322  ssfz12  48478  nnmul2b  48495  iccpartnel  48614  poprelb  48700  lighneal  48790  tgoldbach  49009  clnbgrgrim  49126  lidldomn1  49422  rngccatidALTV  49463  ringccatidALTV  49497  ply1mulgsumlem1  49592  lindslinindsimp2  49669  nn0sumshdiglemA  49825  nn0sumshdiglemB  49826