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

Theorem syl12anc 1226
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
syl12anc.4
Assertion
Ref Expression
syl12anc

Proof of Theorem syl12anc
StepHypRef Expression
1 sylXanc.1 . . 3
2 sylXanc.2 . . 3
3 sylXanc.3 . . 3
41, 2, 3jca32 535 . 2
5 syl12anc.4 . 2
64, 5syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  syl22anc  1229  raaan  3937  raaanv  3938  soltmin  5411  xpdifid  5440  f1dom3fv3dif  6175  cocan1  6194  fliftfun  6210  soisores  6223  soisoi  6224  isopolem  6241  f1oiso2  6248  weniso  6250  caovcld  6468  caovcomd  6471  onminex  6642  tfrlem12  7077  omeulem1  7250  oaabs2  7313  omabs  7315  erov  7427  findcard2d  7782  frfi  7785  finsschain  7847  suplub2  7941  supmaxOLD  7946  supgtoreq  7949  supisolem  7952  ordiso2  7961  ordtypelem7  7970  wemaplem2  7993  wemapsolem  7996  cantnflt  8112  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1  8129  cantnfltOLD  8142  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1OLD  8152  wemapwe  8160  wemapweOLD  8161  cnfcomlem  8164  cnfcom  8165  cnfcom3lem  8168  cnfcomlemOLD  8172  cnfcomOLD  8173  cnfcom3lemOLD  8176  infxpenlem  8412  fseqenlem1  8426  dfac12lem2  8545  infpssrlem4  8707  enfin2i  8722  isf34lem7  8780  isf34lem6  8781  fin1a2lem7  8807  fin1a2lem10  8810  fin1a2lem11  8811  fin1a2lem13  8813  ttukeylem6  8915  ttukeylem7  8916  iundom2g  8936  fpwwe2lem6  9034  fpwwe2lem7  9035  fpwwe2lem9  9037  fpwwe2lem12  9040  fpwwe2  9042  canthnumlem  9047  canthwelem  9049  canthp1lem2  9052  pwfseqlem4  9061  inar1  9174  intgru  9213  distrlem4pr  9425  conjmul  10286  lediv12a  10463  recp1lt1  10468  cju  10557  gtndiv  10965  zsupss  11200  uzsupss  11203  icc0  11606  iccssioo2  11626  fzrev3  11774  elfz1b  11777  fldiv  11987  modabs  12029  addmodid  12036  modltm1p1mod  12039  modifeq2int  12049  seqcaopr  12144  seqf1olem1  12146  seqof2  12165  crreczi  12291  seqcoll  12512  seqcoll2  12513  hashtpg  12523  swrdccat3b  12721  sqrlem2  13077  resqrex  13084  abs1m  13168  isercoll  13490  zsum  13540  fsum2dlem  13585  fsumcom2  13589  fprod2dlem  13784  fprodcom2  13788  efsub  13835  bitsinv2  14093  sqgcd  14196  qredeu  14248  pcpremul  14367  pceulem  14369  pczpre  14371  pcdiv  14376  pcqmul  14377  pcqdiv  14381  pcexp  14383  pcdvdsb  14392  pcneg  14397  pcdvdstr  14399  pcgcd1  14400  pc2dvds  14402  pcz  14404  pcaddlem  14407  pcadd  14408  qexpz  14420  expnprm  14421  infpnlem2  14429  ramub2  14532  ramub1lem1  14544  f1ocpbllem  14921  f1ovscpbl  14923  mreexexlem3d  15043  mreexexlem4d  15044  fthi  15287  ipodrsima  15795  mndpropd  15946  grpsubpropd2  16141  ghmf1  16295  symgfvne  16413  f1omvdmvd  16468  f1otrspeq  16472  pmtrdifwrdel  16510  pmtrdifwrdel2  16511  psgnunilem2  16520  psgnunilem3  16521  psgnvalii  16534  odf1  16584  lsmpropd  16695  gsummptshft  16956  dprdf1o  17079  pgpfac1lem3  17128  pgpfac1lem5  17130  pgpfaclem1  17132  ablfaclem2  17137  srgbinomlem3  17193  ringpropd  17230  f1rhm0to0  17389  lmodprop2d  17572  lsspropd  17663  lmhmpropd  17719  lbspropd  17745  lbsextlem3  17806  lidlsubclOLD  17864  assapropd  17976  psrass1  18060  psrass23l  18063  psrass23  18065  mplsubrg  18102  mplmon  18125  mplmonmul  18126  mplcoe1  18127  mplbas2  18134  mplind  18167  evlslem2  18180  mpfind  18205  gsumply1subr  18275  psrplusgpropd  18277  ply1scln0  18332  ply1coeOLD  18338  iporthcom  18670  obslbs  18761  scmataddcl  19018  scmatsubcl  19019  scmatmulcl  19020  smatvscl  19026  scmatrhmcl  19030  mat1scmat  19041  smadiadetglem2  19174  cramerimplem2  19186  cramerimplem3  19187  cramerimp  19188  1pmatscmul  19203  mat2pmatf1  19230  pm2mp  19326  chmatcl  19329  chmatval  19330  chmaidscmat  19349  chfacfisf  19355  cayhamlem1  19367  cpmidgsumm2pm  19370  cpmidpmat  19374  cpmadugsumfi  19378  cpmadumatpoly  19384  cayhamlem3  19388  pptbas  19509  elcls  19574  neiint  19605  neiptopnei  19633  restbas  19659  neitr  19681  iscnp4  19764  cnconst2  19784  cnpdis  19794  cnt0  19847  cnhaus  19855  cmpcovf  19891  hauscmplem  19906  concompid  19932  2ndci  19949  2ndc1stc  19952  1stcrest  19954  2ndcctbss  19956  2ndcomap  19959  2ndcsep  19960  dis2ndc  19961  restlly  19984  islly2  19985  lly1stc  19997  dislly  19998  finlocfin  20021  dissnlocfin  20030  locfindis  20031  llycmpkgen2  20051  ptbasfi  20082  neitx  20108  ptpjopn  20113  ptcnplem  20122  upxp  20124  txlly  20137  txtube  20141  tx1stc  20151  txkgen  20153  xkococnlem  20160  kqreglem1  20242  kqreglem2  20243  kqnrmlem1  20244  kqnrmlem2  20245  hmeoimaf1o  20271  reghmph  20294  nrmhmph  20295  ordthmeolem  20302  trfil2  20388  fmfnfm  20459  hauspwpwf1  20488  fclsfnflim  20528  cnextf  20566  cnextcn  20567  tmdgsum2  20595  symgtgp  20600  subgntr  20605  opnsubg  20606  ghmcnp  20613  qustgpopn  20618  tsmsf1o  20647  tsmsxplem1  20655  tsmsxplem2  20656  tsmsxp  20657  ustexsym  20718  restutop  20740  imasdsf1olem  20876  blssexps  20929  blssex  20930  ssblex  20931  imasf1oxms  20992  blcld  21008  stdbdmopn  21021  met1stc  21024  met2ndci  21025  prdsxmslem2  21032  metcnp3  21043  cfilucfilOLD  21072  cfilucfil  21073  ngptgp  21150  tgioo  21301  tgqioo  21305  zdis  21321  iccpnfhmeo  21445  xrhmeo  21446  cnheibor  21455  elpi1i  21546  cmetcuspOLD  21793  cmetcusp  21794  pjthlem2  21853  ivthlem2  21864  ovolicc1  21927  ovolicc2lem3  21930  ovolicc2lem4  21931  volsup  21966  volivth  22016  vitalilem3  22019  mbflimsup  22073  mbfi1fseqlem1  22122  mbfi1fseqlem3  22124  mbfi1fseqlem5  22126  limcnlp  22282  limcflf  22285  limciun  22298  dvmptfsum  22376  dvcnvlem  22377  dvcvx  22421  facth1  22565  elply2  22593  plypf1  22609  coeeq  22624  aaliou3lem8  22741  ulm2  22780  mtestbdd  22800  reeff1o  22842  dcubic2  23175  quart  23192  xrlimcnp  23298  amgm  23320  harmonicbnd4  23340  perfect  23506  dchrptlem1  23539  bposlem2  23560  lgsfcl2  23577  lgsdir  23605  lgsdi  23607  lgsne0  23608  dchrvmasumlem2  23683  chpdifbndlem2  23739  pntpbnd1  23771  pntpbnd2  23772  padicabv  23815  tgcgrxfr  23909  idmot  23924  legid  23974  btwnleg  23975  leg0  23979  tghilbert1_1  24017  mirreu3  24035  colperpex  24107  lnopp2hpgb  24132  axcgrrflx  24217  axsegconlem1  24220  axcontlem2  24268  axcontlem12  24278  eengtrkg  24288  nbgraf1olem5  24445  wwlknredwwlkn  24726  clwwlkel  24793  clwlkfclwwlk  24844  2spotiundisj  25062  numclwwlkovf2ex  25086  frgraogt3nreg  25120  subgoid  25309  subgoinv  25310  ghgrpOLD  25370  nvpi  25569  nmlno0lem  25708  fh1  26536  fh2  26537  eigposi  26755  nmlnop0iALT  26914  nmopun  26933  branmfn  27024  opsqrlem1  27059  opsqrlem6  27064  mdslmd1lem1  27244  csmdsymi  27253  atom1d  27272  chirredlem2  27310  cdj1i  27352  cdj3i  27360  fcnvgreu  27514  xrofsup  27582  2sqmod  27636  archirngz  27733  archiabllem2a  27738  orngsqr  27794  ornglmullt  27797  orngrmullt  27798  metideq  27872  metider  27873  pstmfval  27875  lmxrge0  27934  qqhval2  27963  qqhf  27967  qqhghm  27969  qqhrhm  27970  esumpcvgval  28084  sigainb  28136  insiga  28137  ddemeas  28208  imambfm  28233  dya2icoseg  28248  dya2iocnrect  28252  eulerpartlemgvv  28315  probun  28358  ballotlemfc0  28431  ballotlemfcc  28432  sgnmul  28481  signstfvneq0  28529  erdszelem8  28642  erdszelem9  28643  erdsze2lem2  28648  cnpcon  28675  txpcon  28677  ptpcon  28678  indispcon  28679  conpcon  28680  cvxpcon  28687  cnllyscon  28690  cvmcov2  28720  cvmopnlem  28723  cvmliftmolem1  28726  cvmliftlem14  28742  cvmliftlem15  28743  cvmlift2lem13  28760  cvmlift3lem2  28765  cvmlift3lem9  28772  poseq  29333  sltres  29424  nodense  29449  nocvxmin  29451  nobndup  29460  nobnddown  29461  seglerflx  29762  seglemin  29763  btwnsegle  29767  hilbert1.1  29804  wl-2sb6d  30008  tan2h  30047  heicant  30049  mblfinlem2  30052  itg2addnc  30069  ftc2nc  30099  dvasin  30103  neibastop2lem  30178  sdclem1  30236  fdc  30238  istotbnd3  30267  sstotbnd  30271  prdstotbnd  30290  prdsbnd2  30291  cntotbnd  30292  rngoisocnv  30384  mzpcompact2lem  30684  diophrw  30692  rexrabdioph  30727  eldioph4b  30745  pellexlem5  30769  pellfund14  30834  acongtr  30916  fnwe2lem3  30998  gicabl  31047  hbtlem2  31073  hbtlem4  31075  hbtlem5  31077  dgraalem  31094  aaitgo  31111  ioounsn  31177  isprm7  31192  islptre  31625  limclner  31657  icccncfext  31690  stoweidlem1  31783  stoweidlem14  31796  stoweidlem24  31806  stoweidlem46  31828  stoweidlem57  31839  dirkercncflem2  31886  fourierdlem20  31909  fourierdlem41  31930  fourierdlem46  31935  fourierdlem48  31937  fourierdlem50  31939  fourierdlem62  31951  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem76  31965  fourierdlem79  31968  fourierdlem103  31992  fourierdlem104  31993  etransclem47  32064  raaan2  32180  mgmpropd  32463  lidlmmgm  32731  gsumlsscl  32976  lincsumcl  33032  lincscmcl  33033  isldepslvec2  33086  bj-flbi3  34608  bj-finsumval0  34663  lsmsat  34733  islfld  34787  ps-2  35202  lplnexllnN  35288  4atlem9  35327  4atlem10a  35328  lnatexN  35503  2lnat  35508  pmapjat1  35577  lhpj1  35746  lhpm0atN  35753  4atexlemex2  35795  4atex  35800  4atex2-0aOLDN  35802  4atex2-0cOLDN  35804  lautcnvle  35813  lautj  35817  lautm  35818  idltrn  35874  cdleme01N  35946  cdleme0ex1N  35948  cdleme5  35965  cdleme9  35978  cdleme11c  35986  cdleme11g  35990  cdlemefrs29bpre0  36122  cdlemefrs29cpre1  36124  cdlemefrs32fva1  36127  cdleme32fva  36163  cdleme32fva1  36164  cdleme32fvaw  36165  cdleme32d  36170  cdleme32f  36172  cdleme35fnpq  36175  cdleme48d  36261  cdleme48gfv  36263  cdleme50ltrn  36283  trlord  36295  cdlemg4b1  36335  cdlemg4b2  36336  cdlemg13a  36377  cdlemg17a  36387  cdlemg17f  36392  erng1lem  36713  erngdvlem3  36716  erngdvlem4  36717  erng1r  36721  erngdvlem3-rN  36724  erngdvlem4-rN  36725  dva0g  36754  dialss  36773  dia0  36779  dia1N  36780  diaglbN  36782  diameetN  36783  diainN  36784  diaintclN  36785  dia1dim  36788  dia2dimlem5  36795  dia2dimlem7  36797  dia2dimlem9  36799  dia2dimlem10  36800  dia2dimlem12  36802  dia2dimlem13  36803  dvhopvadd  36820  dvhvaddass  36824  dvhopvsca  36829  tendolinv  36832  tendorinv  36833  dvhlveclem  36835  dvh0g  36838  dvheveccl  36839  dvhopN  36843  docaclN  36851  diaocN  36852  djajN  36864  dib0  36891  dib1dim  36892  dibglbN  36893  dibintclN  36894  dib1dim2  36895  diblss  36897  diblsmopel  36898  dicvaddcl  36917  dicvscacl  36918  diclspsn  36921  cdlemn4a  36926  cdlemn11c  36936  dihjustlem  36943  dihord1  36945  dihord2a  36946  dihord2b  36947  dihord2cN  36948  dihord11b  36949  dihord11c  36951  dihord2pre  36952  dihlsscpre  36961  dih1dimb  36967  dib2dim  36970  dih2dimb  36971  dih2dimbALTN  36972  dihvalcq2  36974  dihopelvalcpre  36975  dihord6apre  36983  dihord5b  36986  dihord5apre  36989  dih0  37007  dihmeetlem1N  37017  dihglblem5apreN  37018  dihglblem3N  37022  dihmeetlem2N  37026  dihglbcpreN  37027  dihmeetlem4preN  37033  dih1dimatlem0  37055  dih1dimatlem  37056  dihatlat  37061  dihatexv  37065  dihglb2  37069  dihmeet  37070  dihintcl  37071  dihmeet2  37073  doch2val2  37091  dochocss  37093  dihoml4c  37103  dochdmj1  37117  djhlj  37128  djhljjN  37129  djhjlj  37130  dihsumssj  37135  djhexmid  37138  djhlsmcl  37141  djhcvat42  37142  dihjatcclem4  37148  dihjat1lem  37155  dihsmsprn  37157  dihjat3  37159  dvh3dim2  37175  dvh3dim3N  37176  dochkr1OLDN  37206  lclkrlem2c  37236  lclkrlem2d  37237  mapdpglem23  37421  hdmap11lem2  37572
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
  Copyright terms: Public domain W3C validator