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  4199  unipw  4333  opeluu  4571  uniexb  4594  unon  4633  onintrab2im  4640  xpexg  4864  resiexg  5083  imaexg  5115  exse2  5136  soirri  5157  djudisj  5190  elxp5  5251  cnvexg  5300  cnviinm  5304  coexg  5307  funssres  5395  f1oabexg  5626  sefvex  5691  ssimaex  5738  mptfvex  5763  f1ompt  5828  fmptcof  5844  resfunexg  5905  mptexg  5911  funfvima3  5920  ovid  6170  ov  6173  ofres  6281  cofunexg  6302  opabex3d  6314  opabex3  6315  oprabexd  6320  1stcof  6357  2ndcof  6358  mpoexxg  6406  cnvf1o  6421  f2ndf  6422  algrflemg  6426  tposexg  6489  tfrlemisucaccv  6556  tfrlemibxssdm  6558  tfrlemibfn  6559  tfrlemi14d  6564  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemres  6580  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemres  6593  rdgtfr  6605  rdgruledefgg  6606  rdgon  6617  frecabex  6629  freccllem  6633  frecfcllem  6635  omcl  6694  oeicl  6695  erth  6813  th3qlem1  6871  mapex  6888  pmvalg  6893  mapsnconst  6929  ixpexgg  6957  fundmen  7047  cnvct  7050  mapsnend  7052  snfig  7056  unen  7058  xpdom2  7082  mapxpen  7101  phplem2  7107  findcard2  7146  findcard2s  7147  infnfi  7152  relcnvfi  7208  sbthlemi8  7234  sbthlemi10  7236  fival  7257  fiss  7264  inl11  7356  casef  7379  caseinj  7380  caseinl  7382  caseinr  7383  djudom  7384  difinfsn  7391  djuinj  7397  0ct  7398  ctmlemr  7399  ctssdccl  7402  enomnilem  7429  enmkvlem  7452  enwomnilem  7460  djuassen  7524  xpdjuen  7525  djudoml  7526  djudomr  7527  cc2lem  7580  ltnnnq  7738  nnnq0lem1  7761  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprlemfl  7890  mulnqprlemfu  7891  suplocexprlem2b  8029  prsrlem1  8057  gt0srpr  8063  caucvgsrlemcl  8104  caucvgsrlemfv  8106  caucvgsrlembound  8109  mulcnsr  8150  mulcnsrec  8158  addvalex  8159  pitoregt0  8164  axmulass  8188  axdistr  8189  recriota  8205  mulrid  8271  axmulgt0  8345  cnegexlem2  8449  cnegex  8451  gt0ne0d  8786  recexre  8852  msqge0  8890  mulge0  8893  aptap  8924  recgt0  9124  recreclt  9174  cju  9235  nnge1  9260  nnnlt1  9263  nn0nlt0  9522  nnnle0  9626  elz2  9649  nnm1ge0  9664  recnz  9671  zneo  9679  uz3m2nn  9905  eluz2b2  9935  nn01to3  9949  mnflt  10116  xnn0dcle  10135  xltadd1  10209  lincmb01cmp  10336  iccf1o  10338  fz1n  10378  fseq1p1m1  10428  fznn0  10447  fzctr  10467  4fvwrd4  10474  fzo0n  10502  elfzonlteqm1  10555  divfl0  10656  modqelico  10696  zmodfz  10708  modqid  10711  modqmuladdim  10729  m1modge3gt1  10733  addmodid  10734  frec2uzf1od  10768  frecfzennn  10788  frecfzen2  10789  fzfig  10792  ser0  10895  ser3le  10899  expgt1  10939  expubnd  10958  iexpcyc  11006  binom2sub  11015  binom3  11019  zesq  11020  bernneq  11022  bernneq2  11023  expnbnd  11025  expnlbnd2  11027  facdiv  11100  faclbnd2  11104  faclbnd3  11105  bcval4  11114  hashinfom  11141  hashennn  11143  fihashf1rn  11151  isfinite4im  11155  hashfz  11186  ssenneg  11204  iswrd  11226  iswrdiz  11231  wrdexg  11235  wrdexb  11236  wrdfin  11243  wrdnval  11255  wrdred1hash  11268  ccatsymb  11290  ccatalpha  11301  s111  11319  fzowrddc  11339  swrdlen  11344  swrdwrdsymbg  11356  pfxval  11366  pfx0g  11368  fnpfx  11369  pfxlen  11377  cats1un  11413  swrdccat  11427  crre  11542  crim  11543  remim  11545  mulreap  11549  cjreb  11551  recj  11552  reneg  11553  readd  11554  remullem  11556  imcj  11560  imneg  11561  imadd  11562  cjadd  11569  cjneg  11575  imval2  11579  cjreim  11588  cnrecnv  11595  uzin2  11672  absval  11686  rennim  11687  resqrexlemcalc3  11701  resqrexlemnm  11703  resqrexlemcvg  11704  resqrexlemgt0  11705  resqrexlemga  11708  absreimsq  11752  absreim  11753  amgm2  11803  climconst2  11976  climshft  11989  climshft2  11991  reccn2ap  11998  climge0  12010  sumsnf  12095  sumnul  12110  isumcl  12111  fsum2dlemstep  12120  fisumcom2  12124  fsumabs  12151  fsumiun  12163  binom  12170  bcxmas  12175  arisum  12184  expcnvap0  12188  explecnv  12191  geosergap  12192  geolim  12197  geolim2  12198  geo2sum  12200  geo2lim  12202  cvgratnnlemrate  12216  cvgratz  12218  mertenslemi1  12221  prodf1  12228  prodeq2w  12242  fprodntrivap  12270  prodsnf  12278  fprod2dlemstep  12308  fprodcom2fi  12312  efcllemp  12344  ege2le3  12357  eftlub  12376  efgt1  12383  tanval2ap  12399  tanval3ap  12400  resinval  12401  recosval  12402  efi4p  12403  resin4p  12404  recos4p  12405  resincl  12406  recoscl  12407  efmival  12419  efeul  12420  sinadd  12422  cosadd  12423  tanaddap  12425  sinmul  12430  cos2tsin  12437  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  sin01gt0  12448  cos01gt0  12449  absef  12456  absefib  12457  efieq1re  12458  demoivreALT  12460  eirraplem  12463  3dvds  12550  odd2np1  12559  oddm1even  12561  oddp1even  12562  oexpneg  12563  opoe  12581  omoe  12582  nn0o1gt2  12591  nn0o  12593  bitsdc  12633  bitsfzolem  12640  bitsfzo  12641  bitsinv1lem  12647  bitsinv1  12648  nninfctlemfo  12736  algcvg  12745  algcvgblem  12746  1nprm  12811  1idssfct  12812  oddprmge3  12832  divgcdodd  12840  pw2dvdslemn  12862  pw2dvds  12863  oddpwdclemodd  12869  oddpwdc  12871  phicl2  12911  phibndlem  12913  phibnd  12914  hashdvds  12918  crth  12921  phimullem  12922  eulerthlemfi  12925  eulerthlemrprm  12926  eulerthlema  12927  hashgcdeq  12937  phisum  12938  oddprm  12957  prm23ge5  12962  pythagtriplem1  12963  pythagtriplem4  12966  pythagtriplem12  12973  pythagtriplem14  12975  pczpre  12995  pcadd  13038  pcmpt  13041  pockthlem  13054  pockthi  13056  infpnlem2  13058  gzreim  13077  4sqlem11  13099  4sqlem12  13100  4sqlem13m  13101  4sqlem17  13105  2expltfac  13137  evenennn  13144  ennnfonelemjn  13153  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemnn0  13173  exmidunben  13177  ctinfomlemom  13178  ssnnctlemct  13197  nninfdc  13204  slotex  13239  setscom  13252  strslfv3  13258  setsslid  13263  bassetsnn  13269  basmex  13272  basmexd  13273  relelbasov  13275  ressbas2d  13281  ressbasid  13283  strressid  13284  ressval3d  13285  2strbas1g  13336  2strop1g  13337  rngbaseg  13349  rngplusgg  13350  rngmulrg  13351  srngbased  13360  srngplusgd  13361  srngmulrd  13362  srnginvld  13363  lmodbased  13378  lmodplusgd  13379  lmodscad  13380  lmodvscad  13381  ipsbased  13390  ipsaddgd  13391  ipsmulrd  13392  ipsscad  13393  ipsvscad  13394  ipsipd  13395  topgrpbasd  13410  topgrpplusgd  13411  topgrptsetd  13412  tgvalex  13476  prdsex  13482  prdsval  13486  prdsbaslemss  13487  prdsbas  13489  prdsplusg  13490  prdsmulr  13491  pwsbas  13505  pwselbasb  13506  pwssnf1o  13511  imasex  13518  imasival  13519  imasbas  13520  imasplusg  13521  imasmulr  13522  imasaddfn  13530  imasaddval  13531  imasaddf  13532  imasmulfn  13533  imasmulval  13534  imasmulf  13535  qusval  13536  qusex  13538  qusaddvallemg  13546  qusaddflemg  13547  qusaddval  13548  qusaddf  13549  qusmulval  13550  qusmulf  13551  xpsfval  13561  xpsval  13565  plusffvalg  13575  grpidvalg  13586  igsumvalx  13602  gsumfzval  13604  gsumress  13608  gsum0g  13609  gsumval2  13610  issubmnd  13655  ress0g  13656  ismhm  13674  mhmex  13675  issubm  13685  0mhm  13699  grppropstrg  13732  grpinvfvalg  13755  grpinvval  13756  grpinvfng  13757  grpsubfvalg  13758  grpsubval  13759  grpressid  13774  grplactfval  13814  qusgrp2  13830  mulgfvalg  13838  mulgex  13840  mulgnngsum  13844  issubg  13890  subgex  13893  subgmulg  13905  issubg2m  13906  releqgg  13937  eqgex  13938  eqgfval  13939  eqgen  13944  isghm  13960  ablressid  14052  mgptopng  14073  rngressid  14098  qusrng  14102  dfur2g  14106  ringidss  14173  ring1  14203  ringressid  14207  qusring2  14210  dvdsrvald  14238  dvdsrex  14243  unitgrp  14261  unitabl  14262  invrfvald  14267  unitlinv  14271  unitrinv  14272  dvrfvald  14278  rdivmuldivd  14289  invrpropdg  14294  rhmunitinv  14323  isnzr2  14329  issubrng  14344  issubrg  14366  subrgugrp  14385  subrgpropd  14398  rrgmex  14406  aprval  14428  islmod  14439  scaffvalg  14454  lssex  14502  lssmex  14503  lsssetm  14504  islssmg  14506  islss3  14527  lspfval  14536  lspval  14538  lspcl  14539  lspex  14543  sralemg  14586  srascag  14590  sravscag  14591  sraipg  14592  sraex  14594  rlmsubg  14606  rlmvnegg  14613  ixpsnbasval  14614  lidlvalg  14619  rspvalg  14620  lidlex  14621  rspex  14622  lidlmex  14623  lidlss  14624  lidlrsppropdg  14643  2idlmex  14649  qusrhm  14676  znlidl  14782  zncrng2  14783  znval  14784  znle  14785  znbaslemnn  14787  znbas  14792  znzrh2  14794  znzrhval  14795  znzrhfo  14796  zndvds  14797  znfi  14803  znhash  14804  znidom  14805  znidomb  14806  psrval  14814  psrbasg  14829  psrelbas  14830  psrplusgg  14833  psraddcl  14835  psr0cl  14836  psrnegcl  14838  psr1clfi  14843  mplvalcoe  14845  mplplusgg  14858  toponsspwpwg  14887  topgele  14894  istps  14897  topontopn  14902  tgclb  14930  lmfval  15058  lmres  15113  ispsmet  15188  psmetge0  15196  ismet  15209  isxmet  15210  xmetge0  15230  isxms2  15317  comet  15364  bdxmet  15366  cnmetdval  15394  cnbl0  15399  cnblcld  15400  reopnap  15411  tgioo  15419  cncfcncntop  15458  cncfmpt2fcntop  15464  maxcncf  15480  mincncf  15481  hovergt0  15515  limcimolemlt  15529  cnplimcim  15532  cnplimclemr  15534  limccnpcntop  15540  limccnp2lem  15541  limccnp2cntop  15542  dvfvalap  15546  dvbss  15550  dvcnp2cntop  15564  dvcn  15565  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvrecap  15578  dvmptfsum  15590  dveflem  15591  plyval  15597  plycolemc  15623  dvply2  15632  reeff1olem  15636  pilem3  15648  ef2kpi  15671  efper  15672  sinperlem  15673  efimpi  15684  ptolemy  15689  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  cosq14gt0  15697  tangtx  15703  sinkpi  15712  coskpi  15713  cosordlem  15714  rplogcl  15744  logge0  15745  logdivlti  15746  logbleb  15826  logblt  15827  binom4  15844  wilthlem1  15848  1sgmprm  15862  1sgm2ppw  15863  mersenne  15865  perfect1  15866  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgsval2lem  15883  lgsval4a  15895  lgsneg  15897  lgsdilem  15900  lgsdirprm  15907  lgsdirnn0  15920  gausslemma2dlem0i  15930  gausslemma2dlem6  15940  gausslemma2dlem7  15941  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlemofi  15949  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem2  15955  lgsquad2  15956  m1lgs  15958  2lgs  15977  2lgsoddprmlem2  15979  2lgsoddprm  15986  2sqlem2  15988  vtxvalg  16011  vtxex  16013  struct2slots2dom  16033  structvtxval  16034  structiedg0val  16035  structgrssvtx  16037  structgrssiedg  16038  edgstruct  16059  vdegp1bid  16310  wlkv0  16364  upgr2wlkdc  16372  clwwlkex  16393  clwwlkccatlem  16395  eupthfi  16446  trlsegvdeglem6  16460  konigsberglem1  16483  konigsberglem5  16487  depindlem1  16501  pwf1oexmid  16773  nnnninfex  16800  repiecege0  16811  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837  gfsumsn  16867  gfsump1  16868