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  5369  iunopeqop  5383  predpo  6148  fveqdmss  6842  f1o2ndf1  7828  wfrlem12  7981  fiint  8833  dfac5  9593  ltexprlem7  10507  rpnnen1lem5  12426  fz0fzdiffz0  13070  elfzodifsumelfzo  13157  ssfzo12  13184  elfznelfzo  13196  injresinjlem  13211  addmodlteq  13368  suppssfz  13416  fi1uzind  13912  swrdswrd  14119  cshf1  14224  s3iunsndisj  14380  dfgcd2  15950  cncongr1  16068  infpnlem1  16306  prmgaplem6  16452  initoeu1  17342  termoeu1  17349  cply1mul  21023  pm2mpf1  21504  mp2pm2mplem4  21514  neindisj2  21828  alexsubALTlem3  22754  2sqreultlem  26135  2sqreunnltlem  26138  nbuhgr2vtx1edgblem  27245  cusgrsize2inds  27347  2pthnloop  27624  upgrwlkdvdelem  27629  usgr2pthlem  27656  wwlksnextbi  27784  wspn0  27814  rusgrnumwwlks  27864  clwlkclwwlklem2a  27887  clwlkclwwlklem2  27889  clwwlkf  27936  clwwlknonex2lem2  27997  uhgr3cyclexlem  28070  3cyclfrgrrn1  28174  frgrnbnb  28182  frgrncvvdeqlem9  28196  frgrwopreglem2  28202  frgrregord013  28284  friendship  28288  spansncvi  29539  cdj3lem2b  30324  sat1el2xp  32861  bj-cbvalim  34398  bj-cbvexim  34399  zerdivemp1x  35691  ee233  41626  funbrafv  44110  ssfz12  44267  iccpartnel  44351  poprelb  44437  lighneal  44524  tgoldbach  44730  isomuspgrlem2d  44744  lidldomn1  44940  rngccatidALTV  45008  ringccatidALTV  45071  ply1mulgsumlem1  45188  lindslinindsimp2  45265  nn0sumshdiglemA  45426  nn0sumshdiglemB  45427