Theorem com14 94

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 90	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	com3r 85	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  4895  iunopeqop  4906  predpo  5615  fveqdmss  6262  f1o2ndf1  7172  wfrlem12  7313  fiint  8122  dfac5  8834  ltexprlem7  9743  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  difreicc  12175  fz0fzdiffz0  12317  elfzodifsumelfzo  12401  ssfzo12  12427  elfznelfzo  12439  injresinjlem  12450  addmodlteq  12607  suppssfz  12656  fi1uzind  13134  fi1uzindOLD  13140  swrdswrd  13312  cshf1  13407  s3iunsndisj  13555  dfgcd2  15101  cncongr1  15219  infpnlem1  15452  prmgaplem6  15598  initoeu1  16484  termoeu1  16491  cply1mul  19485  pm2mpf1  20423  mp2pm2mplem4  20433  neindisj2  20737  alexsubALTlem3  21663  nbcusgra  25992  cusgrares  26001  cusgrasize2inds  26005  uvtxnbgra  26021  1pthoncl  26122  wlkdvspthlem  26137  wlkdvspth  26138  usgrcyclnl1  26168  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  wwlknextbi  26253  clwwlkgt0  26299  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwlkf  26322  el2wlkonot  26396  usg2wlkonot  26410  usg2wotspth  26411  cusgraiffrusgra  26467  rusgranumwlks  26483  2pthfrgra  26538  3cyclfrgrarn1  26539  frgranbnb  26547  vdgn0frgrav2  26551  frgrancvvdeqlemC  26566  frg2woteq  26587  usg2spot2nb  26592  numclwlk1lem2foa  26618  frgrareg  26644  frgraregord013  26645  friendship  26649  spansncvi  27895  cdj3lem2b  28680  frrlem11  31036  zerdivemp1x  32916  ee233  37746  funbrafv  39887  iccpartnel  39976  lighneal  40066  tgoldbach  40232  tgoldbachOLD  40239  ssfz12  40351  uhgrauhgrbi  40377  nbuhgr2vtx1edgblem  40573  cusgrsize2inds  40669  2pthnloop  40937  upgrwlkdvdelem  40942  usgr2pthlem  40969  uspgrn2crct  41011  wwlksnextbi  41100  rusgrnumwwlks  41177  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwlksf  41222  clwlksfclwwlk  41269  uhgr3cyclexlem  41348  3cyclfrgrrn1  41455  frgrnbnb  41463  frgrncvvdeqlemC  41478  av-numclwlk1lem2foa  41521  av-frgraregord013  41549  av-friendship  41553  lidldomn1  41711  rngccatidALTV  41781  ringccatidALTV  41844  ply1mulgsumlem1  41968  lindslinindsimp2  42046  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212