Theorem com14 88

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 84	. 2
3	2	com3r 79	1

Syntax hints:  ->wi 4

This theorem is referenced by:  a2andOLD  812  fveqdmss  6026  f1o2ndf1  6908  fiint  7817  dfac5  8530  ltexprlem7  9441  rpnnen1lem5  11241  difreicc  11681  fz0fzdiffz0  11812  elfzodifsumelfzo  11882  ssfzo12  11905  elfznelfzo  11915  injresinjlem  11925  suppssfz  12100  brfi1uzind  12532  swrdswrd  12685  infpnlem1  14428  cply1mul  18335  pm2mpf1  19300  mp2pm2mplem4  19310  neindisj2  19624  alexsubALTlem3  20549  nbcusgra  24463  cusgrares  24472  cusgrasize2inds  24477  uvtxnbgra  24493  1pthoncl  24594  wlkdvspthlem  24609  wlkdvspth  24610  usgrcyclnl1  24640  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  wwlknextbi  24725  clwwlkgt0  24771  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkf  24794  el2wlkonot  24869  usg2wlkonot  24883  usg2wotspth  24884  cusgraiffrusgra  24940  rusgranumwlks  24956  2pthfrgra  25011  3cyclfrgrarn1  25012  frgranbnb  25020  vdgn0frgrav2  25024  frgrancvvdeqlemC  25039  frg2woteq  25060  usg2spot2nb  25065  numclwlk1lem2foa  25091  frgrareg  25117  frgraregord013  25118  friendship  25122  zerdivemp1  25436  spansncvi  26570  cdj3lem2b  27356  predpo  29264  wfrlem12  29354  frrlem11  29399  zerdivemp1x  30358  funbrafv  32243  ssfz12  32330  usgra2pthlem1  32353  uhgrauhgbi  32374  initoeu1  32617  termoeu1  32624  lidldomn1  32727  rngccatidOLD  32797  ringccatidOLD  32860  ply1mulgsumlem1  32986  lindslinindsimp2  33064  ee233  33289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7