Theorem com14 96

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 92	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	com3r 87	1 ⊢ (𝜃 → (𝜓 → (𝜒 → (𝜑 → 𝜏))))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  propeqop  5508  iunopeqop  5522  fveqdmss  7081  f1o2ndf1  8112  wfrlem12OLD  8324  fiint  9328  dfac5  10127  ltexprlem7  11041  rpnnen1lem5  12971  fz0fzdiffz0  13616  elfzodifsumelfzo  13704  ssfzo12  13731  elfznelfzo  13743  injresinjlem  13758  addmodlteq  13917  suppssfz  13965  fi1uzind  14464  swrdswrd  14661  cshf1  14766  s3iunsndisj  14921  dfgcd2  16494  cncongr1  16610  infpnlem1  16849  prmgaplem6  16995  initoeu1  17967  termoeu1  17974  cply1mul  22040  pm2mpf1  22523  mp2pm2mplem4  22533  neindisj2  22849  alexsubALTlem3  23775  2sqreultlem  27184  2sqreunnltlem  27187  nbuhgr2vtx1edgblem  28873  cusgrsize2inds  28975  2pthnloop  29253  upgrwlkdvdelem  29258  usgr2pthlem  29285  wwlksnextbi  29413  wspn0  29443  rusgrnumwwlks  29493  clwlkclwwlklem2a  29516  clwlkclwwlklem2  29518  clwwlkf  29565  clwwlknonex2lem2  29626  uhgr3cyclexlem  29699  3cyclfrgrrn1  29803  frgrnbnb  29811  frgrncvvdeqlem9  29825  frgrwopreglem2  29831  frgrregord013  29913  friendship  29917  spansncvi  31170  cdj3lem2b  31955  sat1el2xp  34666  bj-cbvalim  35827  bj-cbvexim  35828  zerdivemp1x  37120  ee233  43584  funbrafv  46166  ssfz12  46322  iccpartnel  46406  poprelb  46492  lighneal  46579  tgoldbach  46785  isomuspgrlem2d  46799  lidldomn1  46913  rngccatidALTV  46977  ringccatidALTV  47040  ply1mulgsumlem1  47156  lindslinindsimp2  47233  nn0sumshdiglemA  47394  nn0sumshdiglemB  47395