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  5479  iunopeqop  5494  iunopeqopOLD  5495  fveqdmss  7070  f1o2ndf1  8122  fiint  9302  dfac5  10188  ltexprlem7  11108  rpnnen1lem5  13090  fz0fzdiffz0  13751  elfzodifsumelfzo  13846  ssfzo12  13874  elfznelfzo  13888  injresinjlem  13905  addmodlteq  14069  suppssfz  14117  fi1uzind  14632  swrdswrd  14834  cshf1  14941  s3iunsndisj  15101  dfgcd2  16699  cncongr1  16822  infpnlem1  17068  prmgaplem6  17214  initoeu1  18166  termoeu1  18173  cply1mul  22594  pm2mpf1  23097  mp2pm2mplem4  23107  neindisj2  23421  alexsubALTlem3  24348  2sqreultlem  27756  2sqreunnltlem  27759  nbuhgr2vtx1edgblem  29914  cusgrsize2inds  30016  2pthnloop  30299  upgrwlkdvdelem  30304  usgr2pthlem  30331  cyclnumvtx  30370  wwlksnextbi  30465  wspn0  30495  rusgrnumwwlks  30548  clwlkclwwlklem2a  30571  clwlkclwwlklem2  30573  clwwlkf  30620  clwwlknonex2lem2  30681  uhgr3cyclexlem  30764  3cyclfrgrrn1  30868  frgrnbnb  30876  frgrncvvdeqlem9  30890  frgrwopreglem2  30896  frgrregord013  30978  friendship  30982  spansncvi  32236  cdj3lem2b  33021  sat1el2xp  36113  zerdivemp1x  38849  ee233  45461  funbrafv  48172  ssfz12  48328  nnmul2b  48345  iccpartnel  48464  poprelb  48550  lighneal  48640  tgoldbach  48859  clnbgrgrim  48976  lidldomn1  49272  rngccatidALTV  49313  ringccatidALTV  49347  ply1mulgsumlem1  49442  lindslinindsimp2  49519  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676