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  5487  iunopeqop  5501  fveqdmss  7073  f1o2ndf1  8126  wfrlem12OLD  8339  fiint  9343  fiintOLD  9344  dfac5  10148  ltexprlem7  11061  rpnnen1lem5  13002  fz0fzdiffz0  13659  elfzodifsumelfzo  13752  ssfzo12  13780  elfznelfzo  13793  injresinjlem  13808  addmodlteq  13969  suppssfz  14017  fi1uzind  14530  swrdswrd  14728  cshf1  14833  s3iunsndisj  14992  dfgcd2  16570  cncongr1  16691  infpnlem1  16935  prmgaplem6  17081  initoeu1  18029  termoeu1  18036  cply1mul  22239  pm2mpf1  22742  mp2pm2mplem4  22752  neindisj2  23066  alexsubALTlem3  23992  2sqreultlem  27415  2sqreunnltlem  27418  nbuhgr2vtx1edgblem  29335  cusgrsize2inds  29438  2pthnloop  29718  upgrwlkdvdelem  29723  usgr2pthlem  29750  cyclnumvtx  29787  wwlksnextbi  29881  wspn0  29911  rusgrnumwwlks  29961  clwlkclwwlklem2a  29984  clwlkclwwlklem2  29986  clwwlkf  30033  clwwlknonex2lem2  30094  uhgr3cyclexlem  30167  3cyclfrgrrn1  30271  frgrnbnb  30279  frgrncvvdeqlem9  30293  frgrwopreglem2  30299  frgrregord013  30381  friendship  30385  spansncvi  31638  cdj3lem2b  32423  sat1el2xp  35406  bj-cbvalim  36668  bj-cbvexim  36669  zerdivemp1x  37976  ee233  44511  funbrafv  47154  ssfz12  47310  iccpartnel  47419  poprelb  47505  lighneal  47592  tgoldbach  47798  clnbgrgrim  47914  lidldomn1  48173  rngccatidALTV  48214  ringccatidALTV  48248  ply1mulgsumlem1  48329  lindslinindsimp2  48406  nn0sumshdiglemA  48566  nn0sumshdiglemB  48567