Theorem sylancr 414

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancr.1	|- ps
sylancr.2	|- ( ph -> ch )
sylancr.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylancr	|- ( ph -> th )

Proof of Theorem sylancr

Step	Hyp	Ref	Expression
1		sylancr.1	. . 3 |- ps
2	1	a1i 9	. 2 |- ( ph -> ps )
3		sylancr.2	. 2 |- ( ph -> ch )
4		sylancr.3	. 2 |- ( ( ps /\ ch ) -> th )
5	2, 3, 4	syl2anc 411	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpteq2da  4173  unipw  4303  opeluu  4541  uniexb  4564  unon  4603  onintrab2im  4610  xpexg  4833  resiexg  5050  imaexg  5082  exse2  5102  soirri  5123  djudisj  5156  elxp5  5217  cnvexg  5266  cnviinm  5270  coexg  5273  funssres  5360  f1oabexg  5584  sefvex  5648  ssimaex  5695  mptfvex  5720  f1ompt  5786  fmptcof  5802  resfunexg  5860  mptexg  5864  funfvima3  5873  ovid  6121  ov  6124  ofres  6233  cofunexg  6254  opabex3d  6266  opabex3  6267  oprabexd  6272  1stcof  6309  2ndcof  6310  mpoexxg  6356  cnvf1o  6371  f2ndf  6372  algrflemg  6376  tposexg  6404  tfrlemisucaccv  6471  tfrlemibxssdm  6473  tfrlemibfn  6474  tfrlemi14d  6479  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemres  6495  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemres  6508  rdgtfr  6520  rdgruledefgg  6521  rdgon  6532  frecabex  6544  freccllem  6548  frecfcllem  6550  omcl  6607  oeicl  6608  erth  6726  th3qlem1  6784  mapex  6801  pmvalg  6806  mapsnconst  6841  ixpexgg  6869  fundmen  6959  cnvct  6962  snfig  6967  unen  6969  xpdom2  6990  mapxpen  7009  phplem2  7014  findcard2  7051  findcard2s  7052  infnfi  7057  relcnvfi  7108  sbthlemi8  7131  sbthlemi10  7133  fival  7137  fiss  7144  inl11  7232  casef  7255  caseinj  7256  caseinl  7258  caseinr  7259  djudom  7260  difinfsn  7267  djuinj  7273  0ct  7274  ctmlemr  7275  ctssdccl  7278  enomnilem  7305  enmkvlem  7328  enwomnilem  7336  djuassen  7399  xpdjuen  7400  djudoml  7401  djudomr  7402  cc2lem  7452  ltnnnq  7610  nnnq0lem1  7633  addnqprlemfl  7746  addnqprlemfu  7747  mulnqprlemfl  7762  mulnqprlemfu  7763  suplocexprlem2b  7901  prsrlem1  7929  gt0srpr  7935  caucvgsrlemcl  7976  caucvgsrlemfv  7978  caucvgsrlembound  7981  mulcnsr  8022  mulcnsrec  8030  addvalex  8031  pitoregt0  8036  axmulass  8060  axdistr  8061  recriota  8077  mulrid  8143  axmulgt0  8218  cnegexlem2  8322  cnegex  8324  gt0ne0d  8659  recexre  8725  msqge0  8763  mulge0  8766  aptap  8797  recgt0  8997  recreclt  9047  cju  9108  nnge1  9133  nnnlt1  9136  nn0nlt0  9395  nnnle0  9495  elz2  9518  nnm1ge0  9533  recnz  9540  zneo  9548  uz3m2nn  9768  eluz2b2  9798  nn01to3  9812  mnflt  9979  xnn0dcle  9998  xltadd1  10072  lincmb01cmp  10199  iccf1o  10200  fz1n  10240  fseq1p1m1  10290  fznn0  10309  fzctr  10329  4fvwrd4  10336  fzo0n  10364  elfzonlteqm1  10416  divfl0  10516  modqelico  10556  zmodfz  10568  modqid  10571  modqmuladdim  10589  m1modge3gt1  10593  addmodid  10594  frec2uzf1od  10628  frecfzennn  10648  frecfzen2  10649  fzfig  10652  ser0  10755  ser3le  10759  expgt1  10799  expubnd  10818  iexpcyc  10866  binom2sub  10875  binom3  10879  zesq  10880  bernneq  10882  bernneq2  10883  expnbnd  10885  expnlbnd2  10887  facdiv  10960  faclbnd2  10964  faclbnd3  10965  bcval4  10974  hashinfom  11000  hashennn  11002  fihashf1rn  11010  isfinite4im  11014  hashfz  11043  iswrd  11073  iswrdiz  11078  wrdexg  11082  wrdexb  11083  wrdfin  11090  wrdnval  11102  wrdred1hash  11115  ccatsymb  11137  s111  11164  fzowrddc  11179  swrdlen  11184  swrdwrdsymbg  11196  pfxval  11206  pfx0g  11208  fnpfx  11209  pfxlen  11217  cats1un  11253  swrdccat  11267  crre  11368  crim  11369  remim  11371  mulreap  11375  cjreb  11377  recj  11378  reneg  11379  readd  11380  remullem  11382  imcj  11386  imneg  11387  imadd  11388  cjadd  11395  cjneg  11401  imval2  11405  cjreim  11414  cnrecnv  11421  uzin2  11498  absval  11512  rennim  11513  resqrexlemcalc3  11527  resqrexlemnm  11529  resqrexlemcvg  11530  resqrexlemgt0  11531  resqrexlemga  11534  absreimsq  11578  absreim  11579  amgm2  11629  climconst2  11802  climshft  11815  climshft2  11817  reccn2ap  11824  climge0  11836  sumsnf  11920  sumnul  11935  isumcl  11936  fsum2dlemstep  11945  fisumcom2  11949  fsumabs  11976  fsumiun  11988  binom  11995  bcxmas  12000  arisum  12009  expcnvap0  12013  explecnv  12016  geosergap  12017  geolim  12022  geolim2  12023  geo2sum  12025  geo2lim  12027  cvgratnnlemrate  12041  cvgratz  12043  mertenslemi1  12046  prodf1  12053  prodeq2w  12067  fprodntrivap  12095  prodsnf  12103  fprod2dlemstep  12133  fprodcom2fi  12137  efcllemp  12169  ege2le3  12182  eftlub  12201  efgt1  12208  tanval2ap  12224  tanval3ap  12225  resinval  12226  recosval  12227  efi4p  12228  resin4p  12229  recos4p  12230  resincl  12231  recoscl  12232  efmival  12244  efeul  12245  sinadd  12247  cosadd  12248  tanaddap  12250  sinmul  12255  cos2tsin  12262  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  sin01gt0  12273  cos01gt0  12274  absef  12281  absefib  12282  efieq1re  12283  demoivreALT  12285  eirraplem  12288  3dvds  12375  odd2np1  12384  oddm1even  12386  oddp1even  12387  oexpneg  12388  opoe  12406  omoe  12407  nn0o1gt2  12416  nn0o  12418  bitsdc  12458  bitsfzolem  12465  bitsfzo  12466  bitsinv1lem  12472  bitsinv1  12473  nninfctlemfo  12561  algcvg  12570  algcvgblem  12571  1nprm  12636  1idssfct  12637  oddprmge3  12657  divgcdodd  12665  pw2dvdslemn  12687  pw2dvds  12688  oddpwdclemodd  12694  oddpwdc  12696  phicl2  12736  phibndlem  12738  phibnd  12739  hashdvds  12743  crth  12746  phimullem  12747  eulerthlemfi  12750  eulerthlemrprm  12751  eulerthlema  12752  hashgcdeq  12762  phisum  12763  oddprm  12782  prm23ge5  12787  pythagtriplem1  12788  pythagtriplem4  12791  pythagtriplem12  12798  pythagtriplem14  12800  pczpre  12820  pcadd  12863  pcmpt  12866  pockthlem  12879  pockthi  12881  infpnlem2  12883  gzreim  12902  4sqlem11  12924  4sqlem12  12925  4sqlem13m  12926  4sqlem17  12930  2expltfac  12962  evenennn  12964  ennnfonelemjn  12973  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemnn0  12993  exmidunben  12997  ctinfomlemom  12998  ssnnctlemct  13017  nninfdc  13024  slotex  13059  setscom  13072  strslfv3  13078  setsslid  13083  bassetsnn  13089  basmex  13092  basmexd  13093  relelbasov  13095  ressbas2d  13101  ressbasid  13103  strressid  13104  ressval3d  13105  2strbas1g  13156  2strop1g  13157  rngbaseg  13169  rngplusgg  13170  rngmulrg  13171  srngbased  13180  srngplusgd  13181  srngmulrd  13182  srnginvld  13183  lmodbased  13198  lmodplusgd  13199  lmodscad  13200  lmodvscad  13201  ipsbased  13210  ipsaddgd  13211  ipsmulrd  13212  ipsscad  13213  ipsvscad  13214  ipsipd  13215  topgrpbasd  13230  topgrpplusgd  13231  topgrptsetd  13232  tgvalex  13296  prdsex  13302  prdsval  13306  prdsbaslemss  13307  prdsbas  13309  prdsplusg  13310  prdsmulr  13311  pwsbas  13325  pwselbasb  13326  pwssnf1o  13331  imasex  13338  imasival  13339  imasbas  13340  imasplusg  13341  imasmulr  13342  imasaddfn  13350  imasaddval  13351  imasaddf  13352  imasmulfn  13353  imasmulval  13354  imasmulf  13355  qusval  13356  qusex  13358  qusaddvallemg  13366  qusaddflemg  13367  qusaddval  13368  qusaddf  13369  qusmulval  13370  qusmulf  13371  xpsfval  13381  xpsval  13385  plusffvalg  13395  grpidvalg  13406  igsumvalx  13422  gsumfzval  13424  gsumress  13428  gsum0g  13429  gsumval2  13430  issubmnd  13475  ress0g  13476  ismhm  13494  mhmex  13495  issubm  13505  0mhm  13519  grppropstrg  13552  grpinvfvalg  13575  grpinvval  13576  grpinvfng  13577  grpsubfvalg  13578  grpsubval  13579  grpressid  13594  grplactfval  13634  qusgrp2  13650  mulgfvalg  13658  mulgex  13660  mulgnngsum  13664  issubg  13710  subgex  13713  subgmulg  13725  issubg2m  13726  releqgg  13757  eqgex  13758  eqgfval  13759  eqgen  13764  isghm  13780  ablressid  13872  mgptopng  13892  rngressid  13917  qusrng  13921  dfur2g  13925  ringidss  13992  ring1  14022  ringressid  14026  qusring2  14029  dvdsrvald  14057  dvdsrex  14062  unitgrp  14080  unitabl  14081  invrfvald  14086  unitlinv  14090  unitrinv  14091  dvrfvald  14097  rdivmuldivd  14108  invrpropdg  14113  rhmunitinv  14142  isnzr2  14148  issubrng  14163  issubrg  14185  subrgugrp  14204  subrgpropd  14217  rrgmex  14225  aprval  14246  islmod  14255  scaffvalg  14270  lssex  14318  lssmex  14319  lsssetm  14320  islssmg  14322  islss3  14343  lspfval  14352  lspval  14354  lspcl  14355  lspex  14359  sralemg  14402  srascag  14406  sravscag  14407  sraipg  14408  sraex  14410  rlmsubg  14422  rlmvnegg  14429  ixpsnbasval  14430  lidlvalg  14435  rspvalg  14436  lidlex  14437  rspex  14438  lidlmex  14439  lidlss  14440  lidlrsppropdg  14459  2idlmex  14465  qusrhm  14492  znlidl  14598  zncrng2  14599  znval  14600  znle  14601  znbaslemnn  14603  znbas  14608  znzrh2  14610  znzrhval  14611  znzrhfo  14612  zndvds  14613  znfi  14619  znhash  14620  znidom  14621  znidomb  14622  psrval  14630  psrbasg  14638  psrelbas  14639  psrplusgg  14642  psraddcl  14644  psr0cl  14645  psrnegcl  14647  psr1clfi  14652  mplvalcoe  14654  mplplusgg  14667  toponsspwpwg  14696  topgele  14703  istps  14706  topontopn  14711  tgclb  14739  lmfval  14867  lmres  14922  ispsmet  14997  psmetge0  15005  ismet  15018  isxmet  15019  xmetge0  15039  isxms2  15126  comet  15173  bdxmet  15175  cnmetdval  15203  cnbl0  15208  cnblcld  15209  reopnap  15220  tgioo  15228  cncfcncntop  15267  cncfmpt2fcntop  15273  maxcncf  15289  mincncf  15290  hovergt0  15324  limcimolemlt  15338  cnplimcim  15341  cnplimclemr  15343  limccnpcntop  15349  limccnp2lem  15350  limccnp2cntop  15351  dvfvalap  15355  dvbss  15359  dvcnp2cntop  15373  dvcn  15374  dvaddxxbr  15375  dvmulxxbr  15376  dvcoapbr  15381  dvcjbr  15382  dvrecap  15387  dvmptfsum  15399  dveflem  15400  plyval  15406  plycolemc  15432  dvply2  15441  reeff1olem  15445  pilem3  15457  ef2kpi  15480  efper  15481  sinperlem  15482  efimpi  15493  ptolemy  15498  sincosq2sgn  15501  sincosq3sgn  15502  sincosq4sgn  15503  sinq12gt0  15504  cosq14gt0  15506  tangtx  15512  sinkpi  15521  coskpi  15522  cosordlem  15523  rplogcl  15553  logge0  15554  logdivlti  15555  logbleb  15635  logblt  15636  binom4  15653  wilthlem1  15654  1sgmprm  15668  1sgm2ppw  15669  mersenne  15671  perfect1  15672  perfectlem1  15673  perfectlem2  15674  perfect  15675  lgsval2lem  15689  lgsval4a  15701  lgsneg  15703  lgsdilem  15706  lgsdirprm  15713  lgsdirnn0  15726  gausslemma2dlem0i  15736  gausslemma2dlem6  15746  gausslemma2dlem7  15747  gausslemma2d  15748  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgsquadlemofi  15755  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad2lem2  15761  lgsquad2  15762  m1lgs  15764  2lgs  15783  2lgsoddprmlem2  15785  2lgsoddprm  15792  2sqlem2  15794  vtxvalg  15817  vtxex  15819  struct2slots2dom  15839  structvtxval  15840  structiedg0val  15841  structgrssvtx  15843  structgrssiedg  15844  edgstruct  15864  wlkv0  16080  pwf1oexmid  16365  nnnninfex  16388  isomninnlem  16398  iswomninnlem  16417  ismkvnnlem  16420