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  4970  iunopeqop  4981  predpo  5698  fveqdmss  6354  f1o2ndf1  7285  wfrlem12  7426  fiint  8237  dfac5  8951  ltexprlem7  9864  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  difreicc  12304  fz0fzdiffz0  12448  elfzodifsumelfzo  12533  ssfzo12  12561  elfznelfzo  12573  injresinjlem  12588  addmodlteq  12745  suppssfz  12794  fi1uzind  13279  fi1uzindOLD  13285  swrdswrd  13460  cshf1  13556  s3iunsndisj  13707  dfgcd2  15263  cncongr1  15381  infpnlem1  15614  prmgaplem6  15760  initoeu1  16661  termoeu1  16668  cply1mul  19664  pm2mpf1  20604  mp2pm2mplem4  20614  neindisj2  20927  alexsubALTlem3  21853  nbuhgr2vtx1edgblem  26247  cusgrsize2inds  26349  2pthnloop  26627  upgrwlkdvdelem  26632  usgr2pthlem  26659  wwlksnextbi  26789  rusgrnumwwlks  26869  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlksf  26915  clwlksfclwwlk  26962  uhgr3cyclexlem  27041  3cyclfrgrrn1  27149  frgrnbnb  27157  frgrncvvdeqlem9  27171  frgrwopreglem2  27177  numclwwlkovf2exlem2  27212  numclwlk1lem2foa  27224  frgrregord013  27253  friendship  27257  spansncvi  28511  cdj3lem2b  29296  frrlem11  31792  zerdivemp1x  33746  ee233  38725  funbrafv  41238  ssfz12  41324  iccpartnel  41374  lighneal  41528  tgoldbach  41705  tgoldbachOLD  41712  lidldomn1  41921  rngccatidALTV  41989  ringccatidALTV  42052  ply1mulgsumlem1  42174  lindslinindsimp2  42252  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414