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  5506  iunopeqop  5520  fveqdmss  7077  f1o2ndf1  8104  wfrlem12OLD  8316  fiint  9320  dfac5  10119  ltexprlem7  11033  rpnnen1lem5  12961  fz0fzdiffz0  13606  elfzodifsumelfzo  13694  ssfzo12  13721  elfznelfzo  13733  injresinjlem  13748  addmodlteq  13907  suppssfz  13955  fi1uzind  14454  swrdswrd  14651  cshf1  14756  s3iunsndisj  14911  dfgcd2  16484  cncongr1  16600  infpnlem1  16839  prmgaplem6  16985  initoeu1  17957  termoeu1  17964  cply1mul  21809  pm2mpf1  22292  mp2pm2mplem4  22302  neindisj2  22618  alexsubALTlem3  23544  2sqreultlem  26939  2sqreunnltlem  26942  nbuhgr2vtx1edgblem  28597  cusgrsize2inds  28699  2pthnloop  28977  upgrwlkdvdelem  28982  usgr2pthlem  29009  wwlksnextbi  29137  wspn0  29167  rusgrnumwwlks  29217  clwlkclwwlklem2a  29240  clwlkclwwlklem2  29242  clwwlkf  29289  clwwlknonex2lem2  29350  uhgr3cyclexlem  29423  3cyclfrgrrn1  29527  frgrnbnb  29535  frgrncvvdeqlem9  29549  frgrwopreglem2  29555  frgrregord013  29637  friendship  29641  spansncvi  30892  cdj3lem2b  31677  sat1el2xp  34358  bj-cbvalim  35510  bj-cbvexim  35511  zerdivemp1x  36803  ee233  43265  funbrafv  45852  ssfz12  46008  iccpartnel  46092  poprelb  46178  lighneal  46265  tgoldbach  46471  isomuspgrlem2d  46485  lidldomn1  46776  rngccatidALTV  46840  ringccatidALTV  46903  ply1mulgsumlem1  47020  lindslinindsimp2  47097  nn0sumshdiglemA  47258  nn0sumshdiglemB  47259