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  5495  iunopeqop  5509  iunopeqopOLD  5510  fveqdmss  7080  f1o2ndf1  8126  fiint  9296  dfac5  10131  ltexprlem7  11045  rpnnen1lem5  13023  fz0fzdiffz0  13684  elfzodifsumelfzo  13779  ssfzo12  13807  elfznelfzo  13821  injresinjlem  13838  addmodlteq  14002  suppssfz  14050  fi1uzind  14564  swrdswrd  14766  cshf1  14873  s3iunsndisj  15031  dfgcd2  16629  cncongr1  16750  infpnlem1  16995  prmgaplem6  17141  initoeu1  18093  termoeu1  18100  cply1mul  22493  pm2mpf1  22993  mp2pm2mplem4  23003  neindisj2  23317  alexsubALTlem3  24243  2sqreultlem  27648  2sqreunnltlem  27651  nbuhgr2vtx1edgblem  29738  cusgrsize2inds  29840  2pthnloop  30117  upgrwlkdvdelem  30122  usgr2pthlem  30149  cyclnumvtx  30186  wwlksnextbi  30280  wspn0  30310  rusgrnumwwlks  30363  clwlkclwwlklem2a  30386  clwlkclwwlklem2  30388  clwwlkf  30435  clwwlknonex2lem2  30496  uhgr3cyclexlem  30569  3cyclfrgrrn1  30673  frgrnbnb  30681  frgrncvvdeqlem9  30695  frgrwopreglem2  30701  frgrregord013  30783  friendship  30787  spansncvi  32041  cdj3lem2b  32826  sat1el2xp  35892  zerdivemp1x  38639  ee233  45269  funbrafv  47936  ssfz12  48092  nnmul2b  48109  iccpartnel  48228  poprelb  48314  lighneal  48404  tgoldbach  48623  clnbgrgrim  48740  lidldomn1  49037  rngccatidALTV  49078  ringccatidALTV  49112  ply1mulgsumlem1  49207  lindslinindsimp2  49284  nn0sumshdiglemA  49440  nn0sumshdiglemB  49441