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

Theorem syl12anc 1180
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 521 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 15 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  syl22anc  1183  raaan  3574  raaanv  3575  onminex  4614  soltmin  5098  cocan1  5817  fliftfun  5827  soisores  5840  soisoi  5841  isopolem  5858  f1oiso2  5865  weniso  5868  caovcld  6029  caovcomd  6032  tfrlem12  6421  omeulem1  6596  oaabs2  6659  omabs  6661  erov  6771  frfi  7118  finsschain  7178  suplub2  7228  supmax  7232  supisolem  7237  ordiso2  7246  ordtypelem7  7255  wemaplem2  7278  wemapso2lem  7281  cantnflt  7389  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1  7407  wemapwe  7416  cnfcomlem  7418  cnfcom  7419  cnfcom3lem  7422  infxpenlem  7657  fseqenlem1  7667  dfac12lem2  7786  infpssrlem4  7948  enfin2i  7963  isf34lem7  8021  isf34lem6  8022  fin1a2lem7  8048  fin1a2lem10  8051  fin1a2lem11  8052  fin1a2lem13  8054  ttukeylem6  8157  ttukeylem7  8158  iundom2g  8178  fpwwe2lem6  8273  fpwwe2lem7  8274  fpwwe2lem9  8276  fpwwe2lem12  8279  fpwwe2  8281  canthnumlem  8286  canthwelem  8288  canthp1lem2  8291  pwfseqlem4  8300  inar1  8413  intgru  8452  distrlem4pr  8666  conjmul  9493  lediv12a  9665  recp1lt1  9670  lbinfm  9723  cju  9758  gtndiv  10105  zsupss  10323  uzsupss  10326  icc0  10720  iccssioo2  10738  fzrev3  10865  fldiv  10980  modabs  11013  seqcaopr  11099  seqf1olem1  11101  crreczi  11242  seqcoll  11417  seqcoll2  11418  sqrlem2  11745  resqrex  11752  abs1m  11835  isercoll  12157  zsum  12207  fsum2dlem  12249  fsumcom2  12253  efsub  12396  bitsinv2  12650  sqgcd  12753  qredeu  12802  pcpremul  12912  pceulem  12914  pczpre  12916  pcdiv  12921  pcqmul  12922  pcqdiv  12926  pcexp  12928  pcdvdsb  12937  pcneg  12942  pcdvdstr  12944  pcgcd1  12945  pc2dvds  12947  pcz  12949  pcaddlem  12952  pcadd  12953  qexpz  12965  expnprm  12966  infpnlem2  12974  ramub2  13077  ramub1lem1  13089  f1ocpbllem  13442  f1ovscpbl  13444  mreexexlem3d  13564  mreexexlem4d  13565  fthi  13808  ipodrsima  14284  mndpropd  14414  grpsubpropd2  14583  ghmf1  14727  odf1  14891  lsmpropd  15002  dprdf1o  15283  pgpfac1lem3  15328  pgpfac1lem5  15330  pgpfaclem1  15332  ablfaclem2  15337  rngpropd  15388  lmodprop2d  15703  lsspropd  15790  lmhmpropd  15842  lbspropd  15868  lbsextlem3  15929  lidlsubcl  15984  assapropd  16083  mplind  16259  psrplusgpropd  16329  ply1scln0  16382  iporthcom  16555  obslbs  16646  pptbas  16761  elcls  16826  neiint  16857  restbas  16905  cnconst2  17027  cnpdis  17037  cnt0  17090  cnhaus  17098  cmpcovf  17134  hauscmplem  17149  concompid  17173  2ndci  17190  2ndc1stc  17193  1stcrest  17195  2ndcctbss  17197  2ndcomap  17200  2ndcsep  17201  dis2ndc  17202  restlly  17225  islly2  17226  lly1stc  17238  dislly  17239  llycmpkgen2  17261  ptbasfi  17292  ptpjopn  17322  ptcnplem  17331  upxp  17333  txlly  17346  txtube  17350  tx1stc  17360  txkgen  17362  xkococnlem  17369  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  hmeoimaf1o  17477  reghmph  17500  nrmhmph  17501  ordthmeolem  17508  trfil2  17598  fmfnfm  17669  hauspwpwf1  17698  fclsfnflim  17738  tmdgsum2  17795  symgtgp  17800  subgntr  17805  opnsubg  17806  ghmcnp  17813  divstgpopn  17818  tsmsf1o  17843  tsmsxplem1  17851  tsmsxplem2  17852  tsmsxp  17853  imasdsf1olem  17953  blssex  17989  ssblex  17990  imasf1oxms  18051  blcld  18067  stdbdmopn  18080  met1stc  18083  met2ndci  18084  prdsxmslem2  18091  metcnp3  18102  ngptgp  18168  tgioo  18318  tgqioo  18322  zdis  18338  iccpnfhmeo  18459  xrhmeo  18460  cnheibor  18469  elpi1i  18560  pjthlem2  18818  ivthlem2  18828  ovolicc1  18891  ovolicc2lem3  18894  ovolicc2lem4  18895  volsup  18929  volivth  18978  vitalilem3  18981  mbflimsup  19037  mbfi1fseqlem1  19086  mbfi1fseqlem3  19088  mbfi1fseqlem5  19090  limcnlp  19244  limcflf  19247  limciun  19260  dvmptfsum  19338  dvcnvlem  19339  dvcvx  19383  mpfind  19444  facth1  19566  elply2  19594  coeeq  19625  aaliou3lem8  19741  ulm2  19780  reeff1o  19839  dcubic2  20156  quart  20173  xrlimcnp  20279  amgm  20301  harmonicbnd4  20320  perfect  20486  dchrptlem1  20519  bposlem2  20540  lgsfcl2  20557  lgsdir  20585  lgsdi  20587  lgsne0  20588  dchrvmasumlem2  20663  chpdifbndlem2  20719  pntpbnd1  20751  pntpbnd2  20752  padicabv  20795  subgoid  20990  subgoinv  20991  ghgrp  21051  nvpi  21248  nmlno0lem  21387  fh1  22213  fh2  22214  eigposi  22432  nmlnop0iALT  22591  nmopun  22610  branmfn  22701  opsqrlem1  22736  opsqrlem6  22741  mdslmd1lem1  22921  csmdsymi  22930  atom1d  22949  chirredlem2  22987  cdj1i  23029  cdj3i  23037  ifeqeqx  23050  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemsdom  23086  lmxrge0  23390  esumpcvgval  23461  sigainb  23512  insiga  23513  imambfm  23582  erdszelem8  23744  erdszelem9  23745  erdsze2lem2  23750  cnpcon  23776  txpcon  23778  ptpcon  23779  indispcon  23780  conpcon  23781  cvxpcon  23788  cnllyscon  23791  cvmcov2  23821  cvmopnlem  23824  cvmliftmolem1  23827  cvmliftlem14  23843  cvmliftlem15  23844  cvmlift2lem13  23861  cvmlift3lem2  23866  cvmlift3lem9  23873  zprodn0  24162  poseq  24324  sltres  24389  nodense  24414  nocvxmin  24416  nobndup  24425  nobnddown  24426  axcgrrflx  24614  axsegconlem1  24617  axcontlem2  24665  axcontlem12  24675  seglerflx  24807  seglemin  24808  btwnsegle  24812  hilbert1.1  24849  itg2addnclem  25003  itg2addnc  25005  dblsubvec  25577  mvecrtol2  25580  mulinvsca  25583  iscnp4  25666  prdnei  25676  islimrs4  25685  indcls2  26099  pxysxy  26245  finlocfin  26402  locfindis  26408  neibastop2lem  26412  sdclem1  26556  fdc  26558  istotbnd3  26598  sstotbnd  26602  prdstotbnd  26621  prdsbnd2  26622  cntotbnd  26623  rngoisocnv  26715  mzpcompact2lem  26932  diophrw  26941  rexrabdioph  26978  eldioph4b  26997  pellexlem5  27021  pellfund14  27086  acongtr  27168  fnwe2lem3  27252  gicabl  27366  hbtlem2  27431  hbtlem4  27433  hbtlem5  27435  dgraalem  27453  aaitgo  27470  f1omvdmvd  27489  f1otrspeq  27493  psgnunilem2  27521  psgnunilem3  27522  psgnvalii  27535  raaan2  28056  hashtpg  28217  lsmsat  29820  islfld  29874  ps-2  30289  lplnexllnN  30375  4atlem9  30414  4atlem10a  30415  lnatexN  30590  2lnat  30595  pmapjat1  30664  lhpj1  30833  lhpm0atN  30840  4atexlemex2  30882  4atex  30887  4atex2-0aOLDN  30889  4atex2-0cOLDN  30891  lautcnvle  30900  lautj  30904  lautm  30905  idltrn  30961  cdleme01N  31032  cdleme0ex1N  31034  cdleme5  31051  cdleme9  31064  cdleme11c  31072  cdleme11g  31076  cdlemefrs29bpre0  31207  cdlemefrs29cpre1  31209  cdlemefrs32fva1  31212  cdleme32fva  31248  cdleme32fva1  31249  cdleme32fvaw  31250  cdleme32d  31255  cdleme32f  31257  cdleme35fnpq  31260  cdleme48d  31346  cdleme48gfv  31348  cdleme50ltrn  31368  trlord  31380  cdlemg4b1  31420  cdlemg4b2  31421  cdlemg13a  31462  cdlemg17a  31472  cdlemg17f  31477  erng1lem  31798  erngdvlem3  31801  erngdvlem4  31802  erng1r  31806  erngdvlem3-rN  31809  erngdvlem4-rN  31810  dva0g  31839  dialss  31858  dia0  31864  dia1N  31865  diaglbN  31867  diameetN  31868  diainN  31869  diaintclN  31870  dia1dim  31873  dia2dimlem5  31880  dia2dimlem7  31882  dia2dimlem9  31884  dia2dimlem10  31885  dia2dimlem12  31887  dia2dimlem13  31888  dvhopvadd  31905  dvhvaddass  31909  dvhopvsca  31914  tendolinv  31917  tendorinv  31918  dvhlveclem  31920  dvh0g  31923  dvheveccl  31924  dvhopN  31928  docaclN  31936  diaocN  31937  djajN  31949  dib0  31976  dib1dim  31977  dibglbN  31978  dibintclN  31979  dib1dim2  31980  diblss  31982  diblsmopel  31983  dicvaddcl  32002  dicvscacl  32003  diclspsn  32006  cdlemn4a  32011  cdlemn11c  32021  dihjustlem  32028  dihord1  32030  dihord2a  32031  dihord2b  32032  dihord2cN  32033  dihord11b  32034  dihord11c  32036  dihord2pre  32037  dihlsscpre  32046  dih1dimb  32052  dib2dim  32055  dih2dimb  32056  dih2dimbALTN  32057  dihvalcq2  32059  dihopelvalcpre  32060  dihord6apre  32068  dihord5b  32071  dihord5apre  32074  dih0  32092  dihmeetlem1N  32102  dihglblem5apreN  32103  dihglblem3N  32107  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetlem4preN  32118  dih1dimatlem0  32140  dih1dimatlem  32141  dihatlat  32146  dihatexv  32150  dihglb2  32154  dihmeet  32155  dihintcl  32156  dihmeet2  32158  doch2val2  32176  dochocss  32178  dihoml4c  32188  dochdmj1  32202  djhlj  32213  djhljjN  32214  djhjlj  32215  dihsumssj  32220  djhexmid  32223  djhlsmcl  32226  djhcvat42  32227  dihjatcclem4  32233  dihjat1lem  32240  dihsmsprn  32242  dihjat3  32244  dvh3dim2  32260  dvh3dim3N  32261  dochkr1OLDN  32291  lclkrlem2c  32321  lclkrlem2d  32322  mapdpglem23  32506  hdmap11lem2  32657
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 177  df-an 360
  Copyright terms: Public domain W3C validator