MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl13anc Unicode version

Theorem syl13anc 1230
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
syl13anc.5
Assertion
Ref Expression
syl13anc

Proof of Theorem syl13anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . . 3
3 sylXanc.3 . . 3
4 sylXanc.4 . . 3
52, 3, 43jca 1176 . 2
6 syl13anc.5 . 2
71, 5, 6syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  syl23anc  1235  syl33anc  1243  pm2.61da3neOLD  2778  disjxiun  4449  wereu2  4881  ordelord  4905  caovassd  6474  caovcand  6477  caovordid  6481  caovordd  6483  caovdid  6490  caovdird  6493  swoer  7358  swoord1  7359  swoord2  7360  frfi  7785  indexfi  7848  ssfii  7899  elfiun  7910  suplub2  7941  supgtoreq  7949  wemaplem2  7993  htalem  8335  cofsmo  8670  alephsing  8677  sornom  8678  axdc3lem4  8854  zorn2lem1  8897  ttukeylem6  8915  ttukeylem7  8916  prlem934  9432  supfirege  10550  suprfinzcl  11003  fzosubel3  11877  fsuppmapnn0fiublem  12096  seqsplit  12140  seqcaopr  12144  ccatass  12605  wrdcctswrd  12690  wrdeqcats1  12699  wrdeqs1cat  12700  splid  12729  spllen  12730  splfv1  12731  splfv2a  12732  splval2  12733  swrds2  12883  isercolllem2  13488  fsumiun  13635  zprod  13744  pcgcd1  14400  cshwsidrepswmod0  14579  cshwshashlem2  14581  cshwsdisj  14583  firest  14830  iscatd2  15078  posasymb  15582  joinle  15644  meetle  15658  lattrd  15688  latleeqj1  15693  latjlej1  15695  latjlej12  15697  latnlej2  15701  latjidm  15704  latleeqm1  15709  latmlem1  15711  latmlem12  15713  latmidm  15716  latledi  15719  latjass  15725  latj12  15726  latj13  15728  latj31  15729  latjrot  15730  latj4  15731  mod1ile  15735  lubun  15753  clatleglb  15756  latdisdlem  15819  mnd32g  15935  mnd12g  15936  mnd4g  15937  ismndd  15943  prdsmndd  15953  imasmnd  15958  mrcmndind  15997  gsumspl  16012  grpidrcan  16103  grpidlcan  16104  grpinvinv  16105  grplmulf1o  16112  grpinvssd  16115  grpinvadd  16116  grpsubrcan  16119  grpsubadd  16126  grpaddsubass  16128  grppncan  16129  grpsubsub4  16131  grppnpcan2  16132  grpnpncan  16133  grpnpncan0  16134  grpnnncan2  16135  grplactcnv  16138  mulgnn0dir  16165  mulgdirlem  16166  mulgneg2  16169  mulgnnass  16170  mulgnn0ass  16171  mulgass  16172  imasgrp  16186  mhmmnd  16192  nsgconj  16234  isnsg3  16235  nmzsubg  16242  ssnmz  16243  eqger  16251  eqgcpbl  16255  conjghm  16297  conjnmz  16300  conjnmzb  16301  subgga  16338  gass  16339  gasubg  16340  galcan  16342  gacan  16343  gapm  16344  gaorber  16346  gastacl  16347  gastacos  16348  cntzsubm  16373  cntzsubg  16374  oppgmnd  16389  symggen  16495  odmodnn0  16564  mndodconglem  16565  odmod  16570  odcong  16573  odmulgid  16576  odbezout  16580  gexdvdsi  16603  gexdvds  16604  sylow1lem2  16619  sylow1lem4  16621  sylow2blem1  16640  sylow2blem2  16641  sylow2blem3  16642  sylow3lem1  16647  sylow3lem2  16648  lsmass  16688  lsmmod  16693  lsmdisj2  16700  subgdisj1  16709  efgredleme  16761  efgredlemc  16763  efgcpbllemb  16773  frgp0  16778  frgpuplem  16790  abl32  16819  abladdsub4  16824  abladdsub  16825  ablpncan2  16826  ablsubsub  16828  mulgdi  16835  mulgsubdi  16838  odadd1  16854  odadd2  16855  gex2abl  16857  oddvdssubg  16861  cygabl  16893  telgsumfzslem  17017  ablfacrp  17117  pgpfac1lem2  17126  pgpfac1lem3a  17127  pgpfac1lem3  17128  pgpfac1lem4  17129  srgmulgass  17182  srgpcomp  17183  srgpcompp  17184  srgpcomppsc  17185  srgbinomlem3  17193  srgbinomlem4  17194  srgbinomlem  17195  csrgbinom  17197  ringcom  17227  ringlz  17235  ringrz  17236  ringnegl  17240  rngnegr  17241  ringmneg1  17242  ringmneg2  17243  ringsubdi  17245  rngsubdir  17246  mulgass2  17247  prdsringd  17261  imasring  17268  opprring  17280  mulgass3  17286  dvdsrtr  17301  dvdsrmul1  17302  unitgrp  17316  dvrass  17339  dvrcan1  17340  dvrcan3  17341  irredrmul  17356  drngmul0or  17417  subrginv  17445  cntzsubr  17461  lmod0vs  17545  lmodvs0  17546  lmodvsmmulgdi  17547  lmodvneg1  17553  lmodvsneg  17554  lmodcom  17556  lmodsubvs  17566  lmodsubdi  17567  lmodsubdir  17568  lssvsubcl  17590  lssvacl  17600  lssvscl  17601  islss3  17605  lss1d  17609  lssintcl  17610  prdslmodd  17615  lmodvsinv  17682  lmodvsinv2  17683  lmhmplusg  17690  lmhmvsca  17691  lsmcl  17729  pj1lmhm  17746  lvecvs0or  17754  lssvs0or  17756  lvecinv  17759  lspsnvs  17760  lspfixed  17774  lspexch  17775  lspsolvlem  17788  lspsolv  17789  lssacsex  17790  lspsnat  17791  lsppratlem1  17793  lsppratlem3  17795  lsppratlem4  17796  lbsextlem2  17805  lbsextlem4  17807  sralmod  17833  2idlcpbl  17882  unitrrg  17942  assa2ass  17971  issubassa  17973  sraassa  17974  asclghm  17987  asclmul1  17988  asclmul2  17989  asclrhm  17991  assamulgscmlem2  17998  psrbagcon  18022  psrbagconcl  18025  psrbagconf1o  18026  gsumbagdiaglem  18027  psrmulcllem  18040  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  psrass1  18060  psrdi  18061  psrdir  18062  psrass23l  18063  psrcom  18064  mplmon2mul  18166  evlslem1  18184  coe1subfv  18307  lply1binomsc  18349  mulgrhm  18532  mulgrhmOLD  18535  cygznlem3  18608  evpmodpmf1o  18632  ipdi  18675  ip2di  18676  ipsubdir  18677  ipsubdi  18678  ip2subdi  18679  ipassr  18681  ipassr2  18682  ip2eq  18688  ocvlss  18703  lsmcss  18723  frlmphl  18812  frlmup1  18832  mamuass  18904  mamudi  18905  mamudir  18906  mamuvs1  18907  mamuvs2  18908  dmatmul  18999  dmatsubcl  19000  scmataddcl  19018  smatvscl  19026  scmatghm  19035  mavmulass  19051  mdetrlin  19104  mdetrsca  19105  mdetralt  19110  mdetunilem7  19120  mdetuni0  19123  matinv  19179  pm2mpghm  19317  chpscmatgsummon  19346  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  chfacfpmmulgsum2  19366  cpmadugsumlemB  19375  cpmadugsumlemC  19376  cpmadugsumlemF  19377  iinopn  19411  subbascn  19755  cnhaus  19855  nrmsep2  19857  nrmsep  19858  regsep2  19877  isreg2  19878  hauscmplem  19906  1stcfb  19946  2ndcctbss  19956  ptbasfi  20082  pthaus  20139  txtube  20141  txhaus  20148  xkohaus  20154  kqnrmlem1  20244  kqnrmlem2  20245  nrmr0reg  20250  nrmhmph  20295  fbssint  20339  infil  20364  fgabs  20380  filcon  20384  filuni  20386  trfil2  20388  trfg  20392  ufprim  20410  elfm3  20451  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  hausflimi  20481  hauspwpwf1  20488  fclsneii  20518  supnfcls  20521  flimfnfcls  20529  fclscmpi  20530  alexsublem  20544  ghmcnp  20613  qustgpopn  20618  psmetsym  20814  psmettri  20815  psmetge0  20816  psmetres2  20818  xmetge0  20847  xmetsym  20850  xmettri  20854  xmetres2  20864  prdsxmetlem  20871  prdsmet  20873  imasdsf1olem  20876  imasf1oxmet  20878  bldisj  20901  xblss2ps  20904  xblss2  20905  xmeter  20936  prdsbl  20994  metustexhalfOLD  21066  metustexhalf  21067  metustOLD  21070  metust  21071  nrmmetd  21095  ngpsubcan  21133  nmmtri  21141  nmrtri  21143  ngptgp  21150  nlmvscnlem2  21194  nrginvrcnlem  21199  metdcnlem  21341  clmmulg  21593  cvsmuleqdivd  21611  cvsdiveqd  21612  cphabscl  21632  cphsqrtcl2  21633  cphsqrtcl3  21634  cphnmf  21642  cph2ass  21659  ipcau2  21677  tchcphlem2  21679  ipcnlem2  21684  cfilfcls  21713  iscau3  21717  iscmet3lem2  21731  iscmet3  21732  relcmpcmet  21755  minveclem2  21841  minveclem4  21847  pjthlem1  21852  pjthlem2  21853  uniioombllem4  21995  dyadmax  22007  itg1addlem4  22106  itg1climres  22121  ply1divex  22537  aalioulem2  22729  amgmlem  23319  dvdsppwf1o  23462  perfect1  23503  perfectlem1  23504  perfectlem2  23505  dchrptlem2  23540  colline  24030  ttgcontlem1  24188  axcontlem9  24275  eengtrkg  24288  eengtrkge  24289  4cycl4dv4e  24668  el2spthonot0  24871  usg2spthonot1  24890  clwlknclwlkdifnum  24961  eupa0  24974  eupares  24975  eupap1  24976  frg2woteu  25055  numclwwlk5  25112  numclwwlk6  25113  grpoidinvlem4  25209  grpoasscan2  25240  grpoinvop  25243  grpopncan  25253  grponpcan  25254  grpopnpcan2  25255  grpodiveq  25258  gxcom  25271  gxnn0add  25276  ghgrpOLD  25370  rngo2  25390  rngolz  25403  rngorz  25404  zerdivemp1  25436  vcm  25464  nvmul0or  25547  nvpncan2  25551  nvnncan  25558  nvdif  25568  nvabs  25576  smcnlem  25607  lnomul  25675  minvecolem2  25791  superpos  27273  ssnnssfz  27597  omndmul2  27702  omndmul3  27703  ogrpaddltbi  27709  ogrpaddltrbid  27711  ogrpsublt  27712  ogrpinvlt  27714  isarchi3  27731  archirngz  27733  archiabllem1a  27735  archiabllem1  27737  archiabllem2a  27738  archiabllem2c  27739  slmdvs0  27768  gsumvsca1  27773  gsumvsca2  27774  dvrdir  27780  rdivmuldivd  27781  dvrcan5  27783  ornglmullt  27797  isarchiofld  27807  rhmdvd  27811  rhmunitinv  27812  locfinref  27844  metideq  27872  metider  27873  pstmxmet  27876  lmxrge0  27934  qqhghm  27969  qqhrhm  27970  measdivcst  28196  oddpwdc  28293  ballotlemiex  28440  wrdsplex  28495  cvmopnlem  28723  cvmliftmolem2  28727  cvmliftlem6  28735  cvmliftlem8  28737  cvmliftlem9  28738  cvmlift2lem9  28756  cvmlift3lem2  28765  cvmlift3lem6  28769  cvmlift3lem7  28770  cvmlift3lem9  28772  nodense  29449  cgrtriv  29652  cgrdegen  29654  cgrextend  29658  segconeq  29660  btwntriv2  29662  btwncomand  29665  btwntriv1  29666  btwnintr  29669  btwnexch3  29670  btwnouttr  29674  btwnexch  29675  trisegint  29678  ifscgr  29694  btwnxfr  29706  colineartriv1  29717  colineartriv2  29718  colinearxfr  29725  fscgr  29730  lineid  29733  idinside  29734  endofsegidand  29736  btwnconn1lem5  29741  btwnconn1lem7  29743  btwnconn1lem11  29747  btwnconn1lem12  29748  btwnconn1lem13  29749  brsegle2  29759  segleantisym  29765  broutsideof2  29772  btwnoutside  29775  outsideoftr  29779  outsideofeq  29780  outsideofeu  29781  outsidele  29782  lineunray  29797  lineelsb2  29798  linecom  29800  linethru  29803  heicant  30049  neibastop1  30177  mettrifi  30250  isbnd3  30280  heibor1lem  30305  bfplem2  30319  ghomdiv  30346  zerdivemp1x  30358  irrapxlem5  30762  aomclem2  31001  isnumbasgrplem2  31053  mpaaeu  31099  mendring  31141  mendlmod  31142  caofcan  31228  stoweidlem18  31800  stoweidlem41  31823  stoweidlem45  31827  stoweidlem55  31837  fourierdlem25  31914  fourierdlem31  31920  fourierdlem37  31926  fourierdlem42  31931  etransclem48  32065  rnglz  32690  ssnn0ssfz  32938  zlmodzxzsub  32949  invginvrid  32960  lmodvsmdi  32975  ply1sclrmsm  32983  lincsum  33030  lincscm  33031  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  ldepsprlem  33073  lincresunit3lem1  33080  lincresunit3lem2  33081  isldepslvec2  33086  lfladdcl  34796  lflvscl  34802  eqlkr3  34826  lkrlsp  34827  lshpkrlem4  34838  oldmm1  34942  olj01  34950  latmassOLD  34954  latm32  34956  latmrot  34957  latm4  34958  olm01  34961  cmtcomlemN  34973  cmtbr3N  34979  cmtbr4N  34980  lecmtN  34981  omlfh1N  34983  atlen0  35035  atnle  35042  atlatmstc  35044  atlatle  35045  cvlexchb1  35055  cvlcvr1  35064  ishlat3N  35079  hlatjass  35094  hlatj12  35095  hlatj32  35096  hlsupr2  35111  hlhgt2  35113  hl0lt1N  35114  hlrelat  35126  hlrelat2  35127  exatleN  35128  hlrelat3  35136  cvrval5  35139  cvrexchlem  35143  cvratlem  35145  cvrat  35146  atcvr0eq  35150  lnnat  35151  atlt  35161  atlelt  35162  2atlt  35163  atexchltN  35165  cvrat3  35166  2atjm  35169  atbtwn  35170  4noncolr3  35177  athgt  35180  3dimlem3a  35184  3dimlem3OLDN  35186  3dimlem4a  35187  3dimlem4OLDN  35189  3dim1  35191  3dim2  35192  1cvratex  35197  ps-1  35201  ps-2  35202  hlatexch3N  35204  hlatexch4  35205  ps-2b  35206  3atlem1  35207  3atlem2  35208  3atlem5  35211  3atlem6  35212  llnnleat  35237  llncmp  35246  2at0mat0  35249  2atmat0  35250  2atm  35251  lplni2  35261  lvolex3N  35262  lplnnle2at  35265  lplnnleat  35266  lplnnlelln  35267  2atnelpln  35268  llncvrlpln  35282  2atmat  35285  lplncmp  35286  lplnexllnN  35288  2llnjaN  35290  2llnm4  35294  2llnmeqat  35295  lvolnle3at  35306  lvolnleat  35307  2atnelvolN  35311  islvol2aN  35316  4atlem3  35320  4atlem3a  35321  4atlem3b  35322  4atlem4a  35323  4atlem4b  35324  4atlem4c  35325  4atlem4d  35326  4atlem10  35330  4atlem11b  35332  4atlem11  35333  4atlem12b  35335  4atlem12  35336  4at2  35338  lplncvrlvol  35340  lvolcmp  35341  2lplnja  35343  dalemqrprot  35372  dalemply  35378  dalemsly  35379  dalemrot  35381  dalemrotyz  35382  dalem1  35383  dalemcea  35384  dalem3  35388  dalem5  35391  dalem8  35394  dalem-cly  35395  dalem11  35398  dalem12  35399  dalem16  35403  dalem17  35404  dalem18  35405  dalem21  35418  dalem24  35421  dalem25  35422  dalem38  35434  dalem39  35435  dalem44  35440  dalem54  35450  dalem55  35451  dalem57  35453  dalem58  35454  dalem59  35455  dalem60  35456  dath2  35461  2atm2atN  35509  2llnma1b  35510  2llnma3r  35512  cdlema1N  35515  cdlemblem  35517  paddasslem5  35548  paddasslem10  35553  paddasslem12  35555  paddasslem13  35556  paddass  35562  padd12N  35563  padd4N  35564  paddss  35569  pmodlem1  35570  pmodl42N  35575  pmapjoin  35576  pmapjlln1  35579  atmod1i2  35583  llnmod1i2  35584  llnexchb2  35593  dalawlem2  35596  dalawlem3  35597  dalawlem5  35599  dalawlem6  35600  dalawlem7  35601  dalawlem8  35602  dalawlem11  35605  dalawlem12  35606  dalawlem13  35607  pclunN  35622  osumcllem1N  35680  pexmidlem3N  35696  lhp2lt  35725  lhp0lt  35727  lhpexle2lem  35733  lhpexle3lem  35735  lhpocnle  35740  lhpj1  35746  lhpmcvr4N  35750  lhp2at0  35756  lhpat3  35770  4atexlemtlw  35791  4atexlemc  35793  4atexlemnclw  35794  4atexlemcnd  35796  lautcvr  35816  lautj  35817  lautm  35818  ltrnm  35855  ltrnj  35856  ltrncvr  35857  trlval3  35912  cdlemc5  35920  cdlemd2  35924  cdlemd3  35925  cdleme0e  35942  cdleme1  35952  cdleme3c  35955  cdleme3g  35959  cdleme3h  35960  cdleme3  35962  cdleme5  35965  cdleme7c  35970  cdleme7d  35971  cdleme7e  35972  cdleme7ga  35973  cdleme7  35974  cdleme9  35978  cdleme11c  35986  cdleme11g  35990  cdleme11k  35993  cdleme11  35995  cdleme12  35996  cdleme15b  36000  cdleme15d  36002  cdleme16d  36006  cdleme16e  36007  cdleme16f  36008  cdleme17b  36012  cdleme18b  36017  cdleme22gb  36019  cdlemednpq  36024  cdleme19a  36029  cdleme20aN  36035  cdleme20bN  36036  cdleme20c  36037  cdleme20d  36038  cdleme20j  36044  cdleme21c  36053  cdleme22aa  36065  cdleme22b  36067  cdleme22cN  36068  cdleme22d  36069  cdleme22e  36070  cdleme22eALTN  36071  cdleme23b  36076  cdleme23c  36077  cdleme28a  36096  cdleme30a  36104  cdlemefs29bpre0N  36142  cdlemefs29bpre1N  36143  cdlemefs29cpre1N  36144  cdlemefs29clN  36145  cdlemefs32fvaN  36148  cdlemefs32fva1  36149  cdleme32b  36168  cdleme32c  36169  cdleme32e  36171  cdleme35a  36174  cdleme35fnpq  36175  cdleme35b  36176  cdleme35f  36180  cdleme36a  36186  cdleme36m  36187  cdleme37m  36188  cdleme39a  36191  cdleme42c  36198  cdleme42i  36209  cdleme42keg  36212  cdleme42mgN  36214  cdleme48bw  36228  cdlemeg46fjgN  36247  cdlemeg46fjv  36249  cdlemeg46req  36255  cdleme50trn1  36275  cdlemf1  36287  cdlemf2  36288  cdlemg1cex  36314  cdlemg2fv2  36326  cdlemg7fvbwN  36333  cdlemg4c  36338  cdlemg4  36343  cdlemg6c  36346  cdlemg8b  36354  cdlemg10c  36365  cdlemg10  36367  cdlemg11b  36368  cdlemg12f  36374  cdlemg13a  36377  cdlemg17a  36387  cdlemg17dALTN  36390  cdlemg18b  36405  cdlemg19a  36409  cdlemg27a  36418  cdlemg27b  36422  cdlemg33b0  36427  cdlemg33a  36432  cdlemg35  36439  trlcolem  36452  cdlemg42  36455  cdlemg46  36461  trljco  36466  tendopltp  36506  cdlemh1  36541  cdlemh2  36542  cdlemi1  36544  cdlemi  36546  cdlemk3  36559  cdlemk10  36569  cdlemk11  36575  cdlemk15  36581  cdlemk1u  36585  cdlemk5u  36587  cdlemk11u  36597  cdlemk39  36642  cdlemkid1  36648  cdlemk50  36678  cdlemk51  36679  erngdvlem3-rN  36724  tendocnv  36748  tendospcanN  36750  dialss  36773  dia2dimlem1  36791  dia2dimlem2  36792  dia2dimlem3  36793  dia2dimlem10  36800  dia2dimlem12  36802  dvhvaddass  36824  dvhlveclem  36835  cdlemm10N  36845  doca2N  36853  djajN  36864  dib1dim2  36895  diblss  36897  diclspsn  36921  cdlemn2  36922  cdlemn10  36933  dihjustlem  36943  dihord1  36945  dihord2a  36946  dihord2pre2  36953  dib2dim  36970  dih2dimb  36971  dih2dimbALTN  36972  dihopelvalcpre  36975  dihord5b  36986  dihord6b  36987  dihord5apre  36989  dihmeetlem1N  37017  dihglblem5apreN  37018  dihglblem2N  37021  dihglbcpreN  37027  dihmeetbclemN  37031  dihmeetlem3N  37032  dihmeetlem6  37036  dih1dimatlem  37056  djhcvat42  37142  dihjatcclem1  37145  dihjatcclem4  37148  dvh4dimat  37165  lcfl7lem  37226  lclkrlem2m  37246  lcfrlem1  37269  lcdvsass  37334  baerlem3lem1  37434  baerlem5alem1  37435  baerlem5blem1  37436  mapdh6gN  37469  mapdh6hN  37470  hdmap1l6g  37544  hdmap1l6h  37545  hdmapneg  37576  hdmap14lem8  37605  hgmapadd  37624  hgmapmul  37625  hgmapvvlem1  37653
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
  Copyright terms: Public domain W3C validator