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  5281  iunopeqop  5295  predpo  6033  fveqdmss  6702  f1o2ndf1  7662  wfrlem12  7809  fiint  8631  dfac5  9389  ltexprlem7  10299  rpnnen1lem5  12219  fz0fzdiffz0  12855  elfzodifsumelfzo  12941  ssfzo12  12968  elfznelfzo  12980  injresinjlem  12995  addmodlteq  13152  suppssfz  13200  fi1uzind  13689  swrdswrd  13891  cshf1  13996  s3iunsndisj  14150  dfgcd2  15711  cncongr1  15828  infpnlem1  16063  prmgaplem6  16209  initoeu1  17088  termoeu1  17095  cply1mul  20133  pm2mpf1  21079  mp2pm2mplem4  21089  neindisj2  21403  alexsubALTlem3  22329  2sqreultlem  25693  2sqreunnltlem  25696  nbuhgr2vtx1edgblem  26804  cusgrsize2inds  26906  2pthnloop  27187  upgrwlkdvdelem  27192  usgr2pthlem  27219  wwlksnextbi  27347  wspn0  27378  rusgrnumwwlks  27428  clwlkclwwlklem2a  27451  clwlkclwwlklem2  27453  clwwlkf  27501  clwwlknonwwlknonb  27560  clwwlknonex2lem2  27562  uhgr3cyclexlem  27635  3cyclfrgrrn1  27744  frgrnbnb  27752  frgrncvvdeqlem9  27766  frgrwopreglem2  27772  frgrregord013  27854  friendship  27858  spansncvi  29108  cdj3lem2b  29893  sat1el2xp  32188  bj-cbvalim  33521  bj-cbvexim  33522  zerdivemp1x  34703  ee233  40344  funbrafv  42827  ssfz12  42984  iccpartnel  43034  poprelb  43122  lighneal  43212  tgoldbach  43418  isomuspgrlem2d  43432  lidldomn1  43624  rngccatidALTV  43692  ringccatidALTV  43755  ply1mulgsumlem1  43874  lindslinindsimp2  43952  nn0sumshdiglemA  44114  nn0sumshdiglemB  44115