Theorem syl122anc 1237

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

Hypotheses

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

Assertion

Ref	Expression
syl122anc

Proof of Theorem syl122anc

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		syl122anc.6	. 2
8	1, 2, 3, 6, 7	syl121anc 1233	1

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

This theorem is referenced by:  divdiv32d  10370  divcan5d  10371  divcan7d  10373  divdiv1d  10376  divdiv2d  10377  seqcoll  12512  wrdeqswrdlsw  12674  cau3lem  13187  eqsqrtd  13200  isercolllem2  13488  isercoll  13490  summolem2a  13537  divrcnv  13664  prodmolem2a  13741  prmind2  14228  divnumden  14281  pceulem  14369  pcqmul  14377  pcqdiv  14381  pcexp  14383  pcaddlem  14407  pcbc  14419  latledi  15719  latjjdi  15733  latjjdir  15734  sylow1lem1  16618  sylow1lem5  16622  efgred2  16771  abladdsub4  16824  ablpnpcan  16830  ghmplusg  16852  frgpnabllem2  16878  isabvd  17469  lmodvs1  17540  lspsolvlem  17788  evlslem1  18184  frgpcyg  18612  ip2di  18676  mdetuni0  19123  cpmadugsumlemB  19375  elptr2  20075  blss2ps  20906  blss2  20907  blssps  20927  blss  20928  xmeter  20936  metdcnlem  21341  lebnumii  21466  minveclem2  21841  pjthlem1  21852  volfiniun  21957  dvfsumrlimge0  22431  lgsdi  23607  ax5seglem3  24234  ax5seglem6  24237  axcontlem8  24274  eengtrkg  24288  gxdi  25298  vacn  25604  minvecolem2  25791  minvecolem4  25796  disjabrex  27443  disjabrexf  27444  slmdvs1  27763  slmd0vs  27767  orngsqr  27794  ornglmulle  27795  orngrmulle  27796  orngmullt  27799  suborng  27805  cgrcomand  29641  cgrcomr  29647  cgrcomland  29649  cgrcomrand  29650  cgrtriv  29652  cgrid2  29653  ofscom  29657  cgrextend  29658  segconeq  29660  btwntriv2  29662  btwnexch3and  29671  btwnouttr2  29672  btwnouttr  29674  btwnexch  29675  btwnexchand  29676  btwndiff  29677  ifscgr  29694  cgrsub  29695  cgrxfr  29705  lineext  29726  endofsegid  29735  btwnconn1lem2  29738  btwnconn1lem3  29739  btwnconn1lem4  29740  btwnconn1lem5  29741  btwnconn1lem7  29743  btwnconn1lem8  29744  btwnconn1lem10  29746  btwnconn1lem11  29747  btwnconn1lem13  29749  btwnconn1lem14  29750  btwnconn3  29753  midofsegid  29754  segcon2  29755  brsegle2  29759  seglecgr12im  29760  seglecgr12  29761  seglerflx  29762  seglemin  29763  segletr  29764  btwnsegle  29767  colinbtwnle  29768  btwnoutside  29775  broutsideof3  29776  outsideoftr  29779  outsideofeq  29780  outsidele  29782  lineunray  29797  lineelsb2  29798  pellfundex  30822  rmxypairf1o  30847  rmxycomplete  30853  rmxyneg  30856  rmxyadd  30857  rmxy1  30858  rmxy0  30859  jm2.22  30937  proot1mul  31156  deg1mhm  31167  stoweidlem7  31789  stoweidlem36  31818  lfladdcl  34796  lshpkrlem4  34838  latmmdiN  34959  latmmdir  34960  hlatj4  35098  4atlem4b  35324  4atlem11  35333  4atlem12  35336  dalem2  35385  dalem-cly  35395  dalem10  35397  dalem23  35420  dalem38  35434  dalem44  35440  dalem55  35451  cdlema1N  35515  paddclN  35566  pmapjoin  35576  dalawlem3  35597  dalawlem5  35599  dalawlem7  35601  dalawlem8  35602  dalawlem11  35605  dalawlem12  35606  lhpexle3lem  35735  4atexlemc  35793  trlnidat  35898  arglem1N  35915  cdlemd9  35931  cdleme0moN  35950  cdleme11c  35986  cdleme11h  35991  cdleme11  35995  cdleme16c  36005  cdleme16f  36008  cdlemeda  36023  cdleme20l2  36047  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme41sn3a  36159  cdleme32fva  36163  cdleme32b  36168  cdleme32c  36169  cdleme32e  36171  cdleme40m  36193  cdleme40n  36194  cdleme42e  36205  cdleme48d  36261  cdlemf2  36288  cdlemf  36289  cdlemg2fv2  36326  cdlemg7fvbwN  36333  cdlemg7fvN  36350  cdlemg9a  36358  cdlemg9b  36359  cdlemg10a  36366  cdlemg12b  36370  cdlemg17b  36388  cdlemg31d  36426  cdlemg33b0  36427  cdlemg33a  36432  ltrnco  36445  ltrncom  36464  cdlemh  36543  cdlemk3  36559  cdlemk12  36576  cdlemk12u  36598  cdlemkfid1N  36647  cdlemk51  36679  cdlemk54  36684  cdlemk43N  36689  cdlemk35u  36690  cdlemk55u1  36691  cdlemk39u1  36693  cdlemk19u1  36695  dia2dimlem10  36800  dvhgrp  36834  dvh0g  36838  cdlemm10N  36845  diblsmopel  36898  cdlemn4  36925  cdlemn6  36929  cdlemn7  36930  dihordlem7  36941  dihord1  36945  dihord2pre  36952  dihvalcqat  36966  dihopelvalcpre  36975  dihord5apre  36989  dihord  36991  dih1  37013  dihglbcpreN  37027  dihjatc1  37038  dihmeetlem13N  37046  dihmeetALTN  37054  dihjatcclem1  37145  baerlem3lem1  37434

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