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  5484  iunopeqop  5499  iunopeqopOLD  5500  fveqdmss  7105  f1o2ndf1  8163  fiint  9349  dfac5  10237  ltexprlem7  11157  rpnnen1lem5  13139  fz0fzdiffz0  13801  elfzodifsumelfzo  13896  ssfzo12  13924  elfznelfzo  13938  injresinjlem  13955  addmodlteq  14119  suppssfz  14167  fi1uzind  14682  swrdswrd  14885  cshf1  14992  s3iunsndisj  15153  dfgcd2  16751  cncongr1  16874  infpnlem1  17120  prmgaplem6  17266  initoeu1  18218  termoeu1  18225  cply1mul  22647  pm2mpf1  23150  mp2pm2mplem4  23160  neindisj2  23474  alexsubALTlem3  24401  2sqreultlem  27807  2sqreunnltlem  27810  nbuhgr2vtx1edgblem  29965  cusgrsize2inds  30067  2pthnloop  30350  upgrwlkdvdelem  30355  usgr2pthlem  30382  cyclnumvtx  30421  wwlksnextbi  30516  wspn0  30546  rusgrnumwwlks  30599  clwlkclwwlklem2a  30622  clwlkclwwlklem2  30624  clwwlkf  30671  clwwlknonex2lem2  30732  uhgr3cyclexlem  30815  3cyclfrgrrn1  30919  frgrnbnb  30927  frgrncvvdeqlem9  30941  frgrwopreglem2  30947  frgrregord013  31029  friendship  31033  spansncvi  32287  cdj3lem2b  33072  sat1el2xp  36324  zerdivemp1x  39084  ee233  45704  funbrafv  48443  ssfz12  48599  nnmul2b  48616  iccpartnel  48735  poprelb  48821  lighneal  48911  tgoldbach  49130  clnbgrgrim  49247  lidldomn1  49543  rngccatidALTV  49584  ringccatidALTV  49618  ply1mulgsumlem1  49713  lindslinindsimp2  49790  nn0sumshdiglemA  49946  nn0sumshdiglemB  49947