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

Theorem syl12anc 1221
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 535 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 16 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  syl22anc  1224  raaan  3930  raaanv  3931  soltmin  5399  f1dom3fv3dif  6156  cocan1  6175  fliftfun  6191  soisores  6204  soisoi  6205  isopolem  6222  f1oiso2  6229  weniso  6231  caovcld  6445  caovcomd  6448  onminex  6615  tfrlem12  7050  omeulem1  7223  oaabs2  7286  omabs  7288  erov  7400  findcard2d  7753  frfi  7756  finsschain  7818  suplub2  7912  supmax  7916  supgtoreq  7919  supisolem  7922  ordiso2  7931  ordtypelem7  7940  wemaplem2  7963  wemapsolem  7966  cantnflt  8082  cantnfp1lem3  8090  cantnflem1b  8096  cantnflem1  8099  cantnfltOLD  8112  cantnfp1lem3OLD  8116  cantnflem1bOLD  8119  cantnflem1OLD  8122  wemapwe  8130  wemapweOLD  8131  cnfcomlem  8134  cnfcom  8135  cnfcom3lem  8138  cnfcomlemOLD  8142  cnfcomOLD  8143  cnfcom3lemOLD  8146  infxpenlem  8382  fseqenlem1  8396  dfac12lem2  8515  infpssrlem4  8677  enfin2i  8692  isf34lem7  8750  isf34lem6  8751  fin1a2lem7  8777  fin1a2lem10  8780  fin1a2lem11  8781  fin1a2lem13  8783  ttukeylem6  8885  ttukeylem7  8886  iundom2g  8906  fpwwe2lem6  9004  fpwwe2lem7  9005  fpwwe2lem9  9007  fpwwe2lem12  9010  fpwwe2  9012  canthnumlem  9017  canthwelem  9019  canthp1lem2  9022  pwfseqlem4  9031  inar1  9144  intgru  9183  distrlem4pr  9395  conjmul  10252  lediv12a  10429  recp1lt1  10434  cju  10523  gtndiv  10929  zsupss  11162  uzsupss  11165  icc0  11568  iccssioo2  11588  fzrev3  11736  elfz1b  11739  fldiv  11945  modabs  11987  addmodid  11994  modltm1p1mod  11997  modifeq2int  12007  seqcaopr  12102  seqf1olem1  12104  seqof2  12123  crreczi  12248  seqcoll  12467  seqcoll2  12468  hashtpg  12478  swrdccat3b  12673  sqrlem2  13029  resqrex  13036  abs1m  13119  isercoll  13441  zsum  13491  fsum2dlem  13536  fsumcom2  13540  efsub  13687  bitsinv2  13943  sqgcd  14046  qredeu  14098  pcpremul  14217  pceulem  14219  pczpre  14221  pcdiv  14226  pcqmul  14227  pcqdiv  14231  pcexp  14233  pcdvdsb  14242  pcneg  14247  pcdvdstr  14249  pcgcd1  14250  pc2dvds  14252  pcz  14254  pcaddlem  14257  pcadd  14258  qexpz  14270  expnprm  14271  infpnlem2  14279  ramub2  14382  ramub1lem1  14394  f1ocpbllem  14770  f1ovscpbl  14772  mreexexlem3d  14892  mreexexlem4d  14893  fthi  15136  ipodrsima  15643  mndpropd  15754  grpsubpropd2  15937  ghmf1  16085  symgfvne  16203  f1omvdmvd  16259  f1otrspeq  16263  pmtrdifwrdel  16301  pmtrdifwrdel2  16302  psgnunilem2  16311  psgnunilem3  16312  psgnvalii  16325  odf1  16375  lsmpropd  16486  gsummptshft  16742  dprdf1o  16864  pgpfac1lem3  16913  pgpfac1lem5  16915  pgpfaclem1  16917  ablfaclem2  16922  srgbinomlem3  16976  rngpropd  17012  f1rhm0to0  17167  lmodprop2d  17350  lsspropd  17441  lmhmpropd  17497  lbspropd  17523  lbsextlem3  17584  lidlsubcl  17641  assapropd  17742  psrass1  17826  psrass23l  17829  psrass23  17831  mplsubrg  17868  mplmon  17891  mplmonmul  17892  mplcoe1  17893  mplbas2  17900  mplind  17933  evlslem2  17946  mpfind  17971  gsumply1subr  18041  psrplusgpropd  18043  ply1scln0  18098  ply1coeOLD  18104  iporthcom  18432  obslbs  18523  scmataddcl  18780  scmatsubcl  18781  scmatmulcl  18782  smatvscl  18788  scmatrhmcl  18792  mat1scmat  18803  smadiadetglem2  18936  cramerimplem2  18948  cramerimplem3  18949  cramerimp  18950  1pmatscmul  18965  mat2pmatf1  18992  pm2mp  19088  chmatcl  19091  chmatval  19092  chmaidscmat  19111  chfacfisf  19117  cayhamlem1  19129  cpmidgsumm2pm  19132  cpmidpmat  19136  cpmadugsumfi  19140  cpmadumatpoly  19146  cayhamlem3  19150  pptbas  19270  elcls  19335  neiint  19366  neiptopnei  19394  restbas  19420  neitr  19442  iscnp4  19525  cnconst2  19545  cnpdis  19555  cnt0  19608  cnhaus  19616  cmpcovf  19652  hauscmplem  19667  concompid  19693  2ndci  19710  2ndc1stc  19713  1stcrest  19715  2ndcctbss  19717  2ndcomap  19720  2ndcsep  19721  dis2ndc  19722  restlly  19745  islly2  19746  lly1stc  19758  dislly  19759  llycmpkgen2  19781  ptbasfi  19812  neitx  19838  ptpjopn  19843  ptcnplem  19852  upxp  19854  txlly  19867  txtube  19871  tx1stc  19881  txkgen  19883  xkococnlem  19890  kqreglem1  19972  kqreglem2  19973  kqnrmlem1  19974  kqnrmlem2  19975  hmeoimaf1o  20001  reghmph  20024  nrmhmph  20025  ordthmeolem  20032  trfil2  20118  fmfnfm  20189  hauspwpwf1  20218  fclsfnflim  20258  cnextf  20296  cnextcn  20297  tmdgsum2  20325  symgtgp  20330  subgntr  20335  opnsubg  20336  ghmcnp  20343  divstgpopn  20348  tsmsf1o  20377  tsmsxplem1  20385  tsmsxplem2  20386  tsmsxp  20387  ustexsym  20448  restutop  20470  imasdsf1olem  20606  blssexps  20659  blssex  20660  ssblex  20661  imasf1oxms  20722  blcld  20738  stdbdmopn  20751  met1stc  20754  met2ndci  20755  prdsxmslem2  20762  metcnp3  20773  cfilucfilOLD  20802  cfilucfil  20803  ngptgp  20880  tgioo  21031  tgqioo  21035  zdis  21051  iccpnfhmeo  21175  xrhmeo  21176  cnheibor  21185  elpi1i  21276  cmetcuspOLD  21523  rrxmet  21565  pjthlem2  21583  ivthlem2  21594  ovolicc1  21657  ovolicc2lem3  21660  ovolicc2lem4  21661  volsup  21696  volivth  21746  vitalilem3  21749  mbflimsup  21803  mbfi1fseqlem1  21852  mbfi1fseqlem3  21854  mbfi1fseqlem5  21856  limcnlp  22012  limcflf  22015  limciun  22028  dvmptfsum  22106  dvcnvlem  22107  dvcvx  22151  facth1  22295  elply2  22323  plypf1  22339  coeeq  22354  aaliou3lem8  22470  ulm2  22509  mtestbdd  22529  reeff1o  22571  dcubic2  22898  quart  22915  xrlimcnp  23021  amgm  23043  harmonicbnd4  23063  perfect  23229  dchrptlem1  23262  bposlem2  23283  lgsfcl2  23300  lgsdir  23328  lgsdi  23330  lgsne0  23331  dchrvmasumlem2  23406  chpdifbndlem2  23462  pntpbnd1  23494  pntpbnd2  23495  padicabv  23538  idmot  23647  legid  23696  btwnleg  23697  leg0  23701  tghilbert1_1  23726  colperpex  23807  axcgrrflx  23888  axsegconlem1  23891  axcontlem2  23939  axcontlem12  23949  eengtrkg  23959  nbgraf1olem5  24109  wwlknredwwlkn  24390  clwwlkel  24457  clwlkfclwwlk  24508  2spotiundisj  24727  numclwwlkovf2ex  24751  frgraogt3nreg  24785  subgoid  24973  subgoinv  24974  ghgrp  25034  nvpi  25233  nmlno0lem  25372  fh1  26200  fh2  26201  eigposi  26419  nmlnop0iALT  26578  nmopun  26597  branmfn  26688  opsqrlem1  26723  opsqrlem6  26728  mdslmd1lem1  26908  csmdsymi  26917  atom1d  26936  chirredlem2  26974  cdj1i  27016  cdj3i  27024  fcnvgreu  27174  archirngz  27383  archiabllem2a  27388  orngsqr  27445  ornglmullt  27448  orngrmullt  27449  metideq  27496  metider  27497  pstmfval  27499  lmxrge0  27558  qqhval2  27587  qqhf  27591  qqhghm  27593  qqhrhm  27594  esumpcvgval  27712  sigainb  27764  insiga  27765  ddemeas  27836  imambfm  27861  dya2icoseg  27876  dya2iocnrect  27880  eulerpartlemgvv  27943  probun  27986  ballotlemfc0  28059  ballotlemfcc  28060  sgnmul  28109  signstfvneq0  28157  erdszelem8  28270  erdszelem9  28271  erdsze2lem2  28276  cnpcon  28303  txpcon  28305  ptpcon  28306  indispcon  28307  conpcon  28308  cvxpcon  28315  cnllyscon  28318  cvmcov2  28348  cvmopnlem  28351  cvmliftmolem1  28354  cvmliftlem14  28370  cvmliftlem15  28371  cvmlift2lem13  28388  cvmlift3lem2  28393  cvmlift3lem9  28400  fprod2dlem  28675  fprodcom2  28679  poseq  28898  sltres  28989  nodense  29014  nocvxmin  29016  nobndup  29025  nobnddown  29026  seglerflx  29327  seglemin  29328  btwnsegle  29332  hilbert1.1  29369  tan2h  29613  heicant  29615  mblfinlem2  29618  itg2addnc  29635  ftc2nc  29665  dvasin  29669  finlocfin  29760  locfindis  29766  neibastop2lem  29770  sdclem1  29828  fdc  29830  istotbnd3  29859  sstotbnd  29863  prdstotbnd  29882  prdsbnd2  29883  cntotbnd  29884  rngoisocnv  29976  mzpcompact2lem  30277  diophrw  30285  rexrabdioph  30320  eldioph4b  30338  pellexlem5  30362  pellfund14  30427  acongtr  30509  fnwe2lem3  30593  gicabl  30642  hbtlem2  30668  hbtlem4  30670  hbtlem5  30672  dgraalem  30690  aaitgo  30707  ioounsn  30773  stoweidlem1  31258  stoweidlem14  31271  stoweidlem24  31281  stoweidlem46  31303  stoweidlem57  31314  fourierdlem20  31384  fourierdlem46  31410  fourierdlem50  31414  fourierdlem63  31427  fourierdlem64  31428  fourierdlem65  31429  fourierdlem76  31440  fourierdlem79  31443  fourierdlem103  31467  fourierdlem104  31468  raaan2  31604  gsumlsscl  31926  lincsumcl  31982  lincscmcl  31983  isldepslvec2  32036  bj-flbi3  33556  bj-finsumval0  33612  lsmsat  33682  islfld  33736  ps-2  34151  lplnexllnN  34237  4atlem9  34276  4atlem10a  34277  lnatexN  34452  2lnat  34457  pmapjat1  34526  lhpj1  34695  lhpm0atN  34702  4atexlemex2  34744  4atex  34749  4atex2-0aOLDN  34751  4atex2-0cOLDN  34753  lautcnvle  34762  lautj  34766  lautm  34767  idltrn  34823  cdleme01N  34894  cdleme0ex1N  34896  cdleme5  34913  cdleme9  34926  cdleme11c  34934  cdleme11g  34938  cdlemefrs29bpre0  35069  cdlemefrs29cpre1  35071  cdlemefrs32fva1  35074  cdleme32fva  35110  cdleme32fva1  35111  cdleme32fvaw  35112  cdleme32d  35117  cdleme32f  35119  cdleme35fnpq  35122  cdleme48d  35208  cdleme48gfv  35210  cdleme50ltrn  35230  trlord  35242  cdlemg4b1  35282  cdlemg4b2  35283  cdlemg13a  35324  cdlemg17a  35334  cdlemg17f  35339  erng1lem  35660  erngdvlem3  35663  erngdvlem4  35664  erng1r  35668  erngdvlem3-rN  35671  erngdvlem4-rN  35672  dva0g  35701  dialss  35720  dia0  35726  dia1N  35727  diaglbN  35729  diameetN  35730  diainN  35731  diaintclN  35732  dia1dim  35735  dia2dimlem5  35742  dia2dimlem7  35744  dia2dimlem9  35746  dia2dimlem10  35747  dia2dimlem12  35749  dia2dimlem13  35750  dvhopvadd  35767  dvhvaddass  35771  dvhopvsca  35776  tendolinv  35779  tendorinv  35780  dvhlveclem  35782  dvh0g  35785  dvheveccl  35786  dvhopN  35790  docaclN  35798  diaocN  35799  djajN  35811  dib0  35838  dib1dim  35839  dibglbN  35840  dibintclN  35841  dib1dim2  35842  diblss  35844  diblsmopel  35845  dicvaddcl  35864  dicvscacl  35865  diclspsn  35868  cdlemn4a  35873  cdlemn11c  35883  dihjustlem  35890  dihord1  35892  dihord2a  35893  dihord2b  35894  dihord2cN  35895  dihord11b  35896  dihord11c  35898  dihord2pre  35899  dihlsscpre  35908  dih1dimb  35914  dib2dim  35917  dih2dimb  35918  dih2dimbALTN  35919  dihvalcq2  35921  dihopelvalcpre  35922  dihord6apre  35930  dihord5b  35933  dihord5apre  35936  dih0  35954  dihmeetlem1N  35964  dihglblem5apreN  35965  dihglblem3N  35969  dihmeetlem2N  35973  dihglbcpreN  35974  dihmeetlem4preN  35980  dih1dimatlem0  36002  dih1dimatlem  36003  dihatlat  36008  dihatexv  36012  dihglb2  36016  dihmeet  36017  dihintcl  36018  dihmeet2  36020  doch2val2  36038  dochocss  36040  dihoml4c  36050  dochdmj1  36064  djhlj  36075  djhljjN  36076  djhjlj  36077  dihsumssj  36082  djhexmid  36085  djhlsmcl  36088  djhcvat42  36089  dihjatcclem4  36095  dihjat1lem  36102  dihsmsprn  36104  dihjat3  36106  dvh3dim2  36122  dvh3dim3N  36123  dochkr1OLDN  36153  lclkrlem2c  36183  lclkrlem2d  36184  mapdpglem23  36368  hdmap11lem2  36519
  Copyright terms: Public domain W3C validator