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  5488  iunopeqop  5502  iunopeqopOLD  5503  fveqdmss  7075  f1o2ndf1  8123  fiint  9300  dfac5  10135  ltexprlem7  11055  rpnnen1lem5  13035  fz0fzdiffz0  13696  elfzodifsumelfzo  13791  ssfzo12  13819  elfznelfzo  13833  injresinjlem  13850  addmodlteq  14014  suppssfz  14062  fi1uzind  14576  swrdswrd  14778  cshf1  14885  s3iunsndisj  15045  dfgcd2  16642  cncongr1  16763  infpnlem1  17008  prmgaplem6  17154  initoeu1  18106  termoeu1  18113  cply1mul  22527  pm2mpf1  23030  mp2pm2mplem4  23040  neindisj2  23354  alexsubALTlem3  24281  2sqreultlem  27691  2sqreunnltlem  27694  nbuhgr2vtx1edgblem  29819  cusgrsize2inds  29921  2pthnloop  30204  upgrwlkdvdelem  30209  usgr2pthlem  30236  cyclnumvtx  30275  wwlksnextbi  30370  wspn0  30400  rusgrnumwwlks  30453  clwlkclwwlklem2a  30476  clwlkclwwlklem2  30478  clwwlkf  30525  clwwlknonex2lem2  30586  uhgr3cyclexlem  30669  3cyclfrgrrn1  30773  frgrnbnb  30781  frgrncvvdeqlem9  30795  frgrwopreglem2  30801  frgrregord013  30883  friendship  30887  spansncvi  32141  cdj3lem2b  32926  sat1el2xp  35966  zerdivemp1x  38705  ee233  45350  funbrafv  48054  ssfz12  48210  nnmul2b  48227  iccpartnel  48346  poprelb  48432  lighneal  48522  tgoldbach  48741  clnbgrgrim  48858  lidldomn1  49154  rngccatidALTV  49195  ringccatidALTV  49229  ply1mulgsumlem1  49324  lindslinindsimp2  49401  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558