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

Theorem syl12anc 1182
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
syl12anc.4  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
Assertion
Ref Expression
syl12anc  |-  ( ph  ->  ta )

Proof of Theorem syl12anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca32 522 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 16 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  syl22anc  1185  raaan  3678  raaanv  3679  onminex  4727  soltmin  5213  cocan1  5963  fliftfun  5973  soisores  5986  soisoi  5987  isopolem  6004  f1oiso2  6011  weniso  6014  caovcld  6179  caovcomd  6182  tfrlem12  6586  omeulem1  6761  oaabs2  6824  omabs  6826  erov  6937  frfi  7288  finsschain  7348  suplub2  7399  supmax  7403  supisolem  7408  ordiso2  7417  ordtypelem7  7426  wemaplem2  7449  wemapso2lem  7452  cantnflt  7560  cantnfp1lem3  7569  cantnflem1b  7575  cantnflem1  7578  wemapwe  7587  cnfcomlem  7589  cnfcom  7590  cnfcom3lem  7593  infxpenlem  7828  fseqenlem1  7838  dfac12lem2  7957  infpssrlem4  8119  enfin2i  8134  isf34lem7  8192  isf34lem6  8193  fin1a2lem7  8219  fin1a2lem10  8222  fin1a2lem11  8223  fin1a2lem13  8225  ttukeylem6  8327  ttukeylem7  8328  iundom2g  8348  fpwwe2lem6  8443  fpwwe2lem7  8444  fpwwe2lem9  8446  fpwwe2lem12  8449  fpwwe2  8451  canthnumlem  8456  canthwelem  8458  canthp1lem2  8461  pwfseqlem4  8470  inar1  8583  intgru  8622  distrlem4pr  8836  conjmul  9663  lediv12a  9835  recp1lt1  9840  cju  9928  gtndiv  10279  zsupss  10497  uzsupss  10500  icc0  10896  iccssioo2  10915  fzrev3  11042  fldiv  11168  modabs  11201  seqcaopr  11287  seqf1olem1  11289  seqof2  11308  crreczi  11431  hashtpg  11618  seqcoll  11639  seqcoll2  11640  sqrlem2  11976  resqrex  11983  abs1m  12066  isercoll  12388  zsum  12439  fsum2dlem  12481  fsumcom2  12485  efsub  12628  bitsinv2  12882  sqgcd  12985  qredeu  13034  pcpremul  13144  pceulem  13146  pczpre  13148  pcdiv  13153  pcqmul  13154  pcqdiv  13158  pcexp  13160  pcdvdsb  13169  pcneg  13174  pcdvdstr  13176  pcgcd1  13177  pc2dvds  13179  pcz  13181  pcaddlem  13184  pcadd  13185  qexpz  13197  expnprm  13198  infpnlem2  13206  ramub2  13309  ramub1lem1  13321  f1ocpbllem  13676  f1ovscpbl  13678  mreexexlem3d  13798  mreexexlem4d  13799  fthi  14042  ipodrsima  14518  mndpropd  14648  grpsubpropd2  14817  ghmf1  14961  odf1  15125  lsmpropd  15236  dprdf1o  15517  pgpfac1lem3  15562  pgpfac1lem5  15564  pgpfaclem1  15566  ablfaclem2  15571  rngpropd  15622  lmodprop2d  15933  lsspropd  16020  lmhmpropd  16072  lbspropd  16098  lbsextlem3  16159  lidlsubcl  16214  assapropd  16313  mplind  16489  psrplusgpropd  16556  ply1scln0  16609  iporthcom  16789  obslbs  16880  pptbas  16995  elcls  17060  neiint  17091  neiptopnei  17119  restbas  17144  neitr  17166  iscnp4  17249  cnconst2  17269  cnpdis  17279  cnt0  17332  cnhaus  17340  cmpcovf  17376  hauscmplem  17391  concompid  17415  2ndci  17432  2ndc1stc  17435  1stcrest  17437  2ndcctbss  17439  2ndcomap  17442  2ndcsep  17443  dis2ndc  17444  restlly  17467  islly2  17468  lly1stc  17480  dislly  17481  llycmpkgen2  17503  ptbasfi  17534  neitx  17560  ptpjopn  17565  ptcnplem  17574  upxp  17576  txlly  17589  txtube  17593  tx1stc  17603  txkgen  17605  xkococnlem  17612  kqreglem1  17694  kqreglem2  17695  kqnrmlem1  17696  kqnrmlem2  17697  hmeoimaf1o  17723  reghmph  17746  nrmhmph  17747  ordthmeolem  17754  trfil2  17840  fmfnfm  17911  hauspwpwf1  17940  fclsfnflim  17980  cnextf  18018  cnextcn  18019  tmdgsum2  18047  symgtgp  18052  subgntr  18057  opnsubg  18058  ghmcnp  18065  divstgpopn  18070  tsmsf1o  18095  tsmsxplem1  18103  tsmsxplem2  18104  tsmsxp  18105  ustexsym  18166  restutop  18188  imasdsf1olem  18311  blssex  18347  ssblex  18348  imasf1oxms  18409  blcld  18425  stdbdmopn  18438  met1stc  18441  met2ndci  18442  prdsxmslem2  18449  metcnp3  18460  cfilucfil  18479  ngptgp  18548  tgioo  18698  tgqioo  18702  zdis  18718  iccpnfhmeo  18841  xrhmeo  18842  cnheibor  18851  elpi1i  18942  cmetcusp  19175  pjthlem2  19206  ivthlem2  19216  ovolicc1  19279  ovolicc2lem3  19282  ovolicc2lem4  19283  volsup  19317  volivth  19366  vitalilem3  19369  mbflimsup  19425  mbfi1fseqlem1  19474  mbfi1fseqlem3  19476  mbfi1fseqlem5  19478  limcnlp  19632  limcflf  19635  limciun  19648  dvmptfsum  19726  dvcnvlem  19727  dvcvx  19771  mpfind  19832  facth1  19954  elply2  19982  coeeq  20013  aaliou3lem8  20129  ulm2  20168  mtestbdd  20188  reeff1o  20230  dcubic2  20551  quart  20568  xrlimcnp  20674  amgm  20696  harmonicbnd4  20716  perfect  20882  dchrptlem1  20915  bposlem2  20936  lgsfcl2  20953  lgsdir  20981  lgsdi  20983  lgsne0  20984  dchrvmasumlem2  21059  chpdifbndlem2  21115  pntpbnd1  21147  pntpbnd2  21148  padicabv  21191  nbgraf1olem5  21321  sizeusglecusg  21361  subgoid  21743  subgoinv  21744  ghgrp  21804  nvpi  22003  nmlno0lem  22142  fh1  22968  fh2  22969  eigposi  23187  nmlnop0iALT  23346  nmopun  23365  branmfn  23456  opsqrlem1  23491  opsqrlem6  23496  mdslmd1lem1  23676  csmdsymi  23685  atom1d  23704  chirredlem2  23742  cdj1i  23784  cdj3i  23792  ofldsqr  24066  lmxrge0  24141  qqhval2  24165  qqhf  24169  qqhghm  24171  qqhrhm  24172  esumpcvgval  24264  sigainb  24315  insiga  24316  imambfm  24406  dya2icoseg  24421  dya2iocnrect  24425  probun  24456  ballotlemfc0  24529  ballotlemfcc  24530  erdszelem8  24663  erdszelem9  24664  erdsze2lem2  24669  cnpcon  24696  txpcon  24698  ptpcon  24699  indispcon  24700  conpcon  24701  cvxpcon  24708  cnllyscon  24711  cvmcov2  24741  cvmopnlem  24744  cvmliftmolem1  24747  cvmliftlem14  24763  cvmliftlem15  24764  cvmlift2lem13  24781  cvmlift3lem2  24786  cvmlift3lem9  24793  poseq  25277  sltres  25342  nodense  25367  nocvxmin  25369  nobndup  25378  nobnddown  25379  axcgrrflx  25567  axsegconlem1  25570  axcontlem2  25618  axcontlem12  25628  seglerflx  25760  seglemin  25761  btwnsegle  25765  hilbert1.1  25802  itg2addnclem  25957  itg2addnc  25959  finlocfin  26070  locfindis  26076  neibastop2lem  26080  sdclem1  26138  fdc  26140  istotbnd3  26171  sstotbnd  26175  prdstotbnd  26194  prdsbnd2  26195  cntotbnd  26196  rngoisocnv  26288  mzpcompact2lem  26499  diophrw  26508  rexrabdioph  26545  eldioph4b  26563  pellexlem5  26587  pellfund14  26652  acongtr  26734  fnwe2lem3  26818  gicabl  26932  hbtlem2  26997  hbtlem4  26999  hbtlem5  27001  dgraalem  27019  aaitgo  27036  f1omvdmvd  27055  f1otrspeq  27059  psgnunilem2  27087  psgnunilem3  27088  psgnvalii  27101  stoweidlem1  27418  stoweidlem14  27431  stoweidlem24  27441  stoweidlem46  27463  stoweidlem57  27474  raaan2  27621  lsmsat  29123  islfld  29177  ps-2  29592  lplnexllnN  29678  4atlem9  29717  4atlem10a  29718  lnatexN  29893  2lnat  29898  pmapjat1  29967  lhpj1  30136  lhpm0atN  30143  4atexlemex2  30185  4atex  30190  4atex2-0aOLDN  30192  4atex2-0cOLDN  30194  lautcnvle  30203  lautj  30207  lautm  30208  idltrn  30264  cdleme01N  30335  cdleme0ex1N  30337  cdleme5  30354  cdleme9  30367  cdleme11c  30375  cdleme11g  30379  cdlemefrs29bpre0  30510  cdlemefrs29cpre1  30512  cdlemefrs32fva1  30515  cdleme32fva  30551  cdleme32fva1  30552  cdleme32fvaw  30553  cdleme32d  30558  cdleme32f  30560  cdleme35fnpq  30563  cdleme48d  30649  cdleme48gfv  30651  cdleme50ltrn  30671  trlord  30683  cdlemg4b1  30723  cdlemg4b2  30724  cdlemg13a  30765  cdlemg17a  30775  cdlemg17f  30780  erng1lem  31101  erngdvlem3  31104  erngdvlem4  31105  erng1r  31109  erngdvlem3-rN  31112  erngdvlem4-rN  31113  dva0g  31142  dialss  31161  dia0  31167  dia1N  31168  diaglbN  31170  diameetN  31171  diainN  31172  diaintclN  31173  dia1dim  31176  dia2dimlem5  31183  dia2dimlem7  31185  dia2dimlem9  31187  dia2dimlem10  31188  dia2dimlem12  31190  dia2dimlem13  31191  dvhopvadd  31208  dvhvaddass  31212  dvhopvsca  31217  tendolinv  31220  tendorinv  31221  dvhlveclem  31223  dvh0g  31226  dvheveccl  31227  dvhopN  31231  docaclN  31239  diaocN  31240  djajN  31252  dib0  31279  dib1dim  31280  dibglbN  31281  dibintclN  31282  dib1dim2  31283  diblss  31285  diblsmopel  31286  dicvaddcl  31305  dicvscacl  31306  diclspsn  31309  cdlemn4a  31314  cdlemn11c  31324  dihjustlem  31331  dihord1  31333  dihord2a  31334  dihord2b  31335  dihord2cN  31336  dihord11b  31337  dihord11c  31339  dihord2pre  31340  dihlsscpre  31349  dih1dimb  31355  dib2dim  31358  dih2dimb  31359  dih2dimbALTN  31360  dihvalcq2  31362  dihopelvalcpre  31363  dihord6apre  31371  dihord5b  31374  dihord5apre  31377  dih0  31395  dihmeetlem1N  31405  dihglblem5apreN  31406  dihglblem3N  31410  dihmeetlem2N  31414  dihglbcpreN  31415  dihmeetlem4preN  31421  dih1dimatlem0  31443  dih1dimatlem  31444  dihatlat  31449  dihatexv  31453  dihglb2  31457  dihmeet  31458  dihintcl  31459  dihmeet2  31461  doch2val2  31479  dochocss  31481  dihoml4c  31491  dochdmj1  31505  djhlj  31516  djhljjN  31517  djhjlj  31518  dihsumssj  31523  djhexmid  31526  djhlsmcl  31529  djhcvat42  31530  dihjatcclem4  31536  dihjat1lem  31543  dihsmsprn  31545  dihjat3  31547  dvh3dim2  31563  dvh3dim3N  31564  dochkr1OLDN  31594  lclkrlem2c  31624  lclkrlem2d  31625  mapdpglem23  31809  hdmap11lem2  31960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator