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  5497  iunopeqop  5511  fveqdmss  7070  f1o2ndf1  8102  wfrlem12OLD  8315  fiint  9320  dfac5  10119  ltexprlem7  11033  rpnnen1lem5  12962  fz0fzdiffz0  13607  elfzodifsumelfzo  13695  ssfzo12  13722  elfznelfzo  13734  injresinjlem  13749  addmodlteq  13908  suppssfz  13956  fi1uzind  14455  swrdswrd  14652  cshf1  14757  s3iunsndisj  14912  dfgcd2  16485  cncongr1  16601  infpnlem1  16842  prmgaplem6  16988  initoeu1  17963  termoeu1  17970  cply1mul  22137  pm2mpf1  22623  mp2pm2mplem4  22633  neindisj2  22949  alexsubALTlem3  23875  2sqreultlem  27296  2sqreunnltlem  27299  nbuhgr2vtx1edgblem  29077  cusgrsize2inds  29179  2pthnloop  29457  upgrwlkdvdelem  29462  usgr2pthlem  29489  wwlksnextbi  29617  wspn0  29647  rusgrnumwwlks  29697  clwlkclwwlklem2a  29720  clwlkclwwlklem2  29722  clwwlkf  29769  clwwlknonex2lem2  29830  uhgr3cyclexlem  29903  3cyclfrgrrn1  30007  frgrnbnb  30015  frgrncvvdeqlem9  30029  frgrwopreglem2  30035  frgrregord013  30117  friendship  30121  spansncvi  31374  cdj3lem2b  32159  sat1el2xp  34859  bj-cbvalim  36012  bj-cbvexim  36013  zerdivemp1x  37305  ee233  43769  funbrafv  46351  ssfz12  46507  iccpartnel  46591  poprelb  46677  lighneal  46764  tgoldbach  46970  isomuspgrlem2d  46984  lidldomn1  47094  rngccatidALTV  47135  ringccatidALTV  47169  ply1mulgsumlem1  47255  lindslinindsimp2  47332  nn0sumshdiglemA  47493  nn0sumshdiglemB  47494