Theorem syl32anc 1236

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
sylXanc.5
syl32anc.6

Assertion

Ref	Expression
syl32anc

Proof of Theorem syl32anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2
2		sylXanc.2	. 2
3		sylXanc.3	. 2
4		sylXanc.4	. . 3
5		sylXanc.5	. . 3
6	4, 5	jca 532	. 2
7		syl32anc.6	. 2
8	1, 2, 3, 6, 7	syl31anc 1231	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  coftr  8674  fin1a2s  8815  snunioo  11675  snunico  11676  snunioc  11677  exple1  12225  leexp2rd  12343  facubnd  12378  permnn  12404  reuccats1  12706  dvdsadd2b  14028  dvdsmulgcd  14192  sqgcd  14196  ramlb  14537  0ram  14538  ram0  14540  ramz2  14542  ramz  14543  ramcl  14547  lsmub1x  16666  lsmub2x  16667  lsmsubm  16673  pgpfac1lem2  17126  mptscmfsupp0  17576  psrass1lem  18029  psrlidm  18056  psrridm  18058  psrcom  18064  mplsubrglem  18100  mvrcl  18111  mplcoe5  18131  mplbas2  18134  psrbagev1  18177  evlslem6  18181  evlslem3  18183  psropprmul  18279  xrsdsreclblem  18464  uvcff  18822  uvcresum  18824  frlmup1  18832  smadiadetg  19175  cayhamlem4  19389  lecldbas  19720  pnfnei  19721  mnfnei  19722  clscon  19931  txcls  20105  ufldom  20463  hauspwpwf1  20488  flfcnp  20505  flfcnp2  20508  cnpfcfi  20541  tsmsmhm  20648  met2ndci  21025  nghmco  21245  nghmplusg  21247  icopnfcld  21275  iocmnfcld  21276  tgioo  21301  reconnlem1  21331  metdseq0  21358  ovolunnul  21911  volinun  21956  volfiniun  21957  volsup  21966  icombl  21974  ioombl  21975  ovolioo  21978  ioorcl2  21981  volivth  22016  ismbf3d  22061  dvferm2lem  22387  lhop  22417  tayl0  22757  pserulm  22817  cxpcn3  23122  ssscongptld  23156  heron  23169  dvdsmulf1o  23470  logexprlim  23500  perfectlem2  23505  lgssq  23610  lgssq2  23611  lgsquad2lem1  23633  lgsquad2lem2  23634  2sqblem  23652  ostth2lem2  23819  ostth3  23823  ubthlem2  25787  nmopleid  27058  numdenneg  27608  2sqcoprm  27635  archirngz  27733  archiabllem1a  27735  locfinreflem  27843  sxbrsigalem2  28257  oddpwdc  28293  ballotlemsdom  28450  ballotlemsel1i  28451  ballotlemsima  28454  ballotlemfrcn0  28468  elmrsubrn  28880  ismblfin  30055  itg2gt0cn  30070  cntotbnd  30292  ismtyhmeolem  30300  heibor1lem  30305  heiborlem6  30312  rrnequiv  30331  bezoutr  30923  jm2.20nn  30939  jm2.25  30941  kercvrlsm  31029  hashgcdlem  31157  binomcxplemnn0  31254  snunioo2  31544  snunioo1  31552  limcleqr  31650  dvdivbd  31720  volioc  31771  iblspltprt  31772  stoweidlem1  31783  stoweidlem20  31802  stoweidlem24  31806  etransclem23  32040  lincresunit2  33079  1cvrat  35200  ps-2b  35206  2at0mat0  35249  ps-2c  35252  llncvrlpln2  35281  2llnmeqat  35295  4atlem10  35330  4atlem11a  35331  4atlem12a  35334  2lplnja  35343  dalemcea  35384  dalem2  35385  dalem21  35418  dalem54  35450  2lnat  35508  cdlemb  35518  elpaddat  35528  paddasslem7  35550  paddasslem9  35552  paddasslem10  35553  paddasslem15  35558  poml6N  35679  osumcllem6N  35685  osumcllem7N  35686  pexmidlem4N  35697  pl42lem4N  35706  lhplt  35724  lhpjat1  35744  cdlemc5  35920  cdlemeg46fgN  36260  cdlemg12g  36375  tendoco2  36494  tendococl  36498  tendodi1  36510  tendoicl  36522  cdlemi2  36545  tendospdi1  36747  dihord11c  36951  dihmeetlem6  37036  dihjatc1  37038  dihmeetlem10N  37043

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975