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  4183  unipw  4315  opeluu  4553  uniexb  4576  unon  4615  onintrab2im  4622  xpexg  4846  resiexg  5064  imaexg  5096  exse2  5117  soirri  5138  djudisj  5171  elxp5  5232  cnvexg  5281  cnviinm  5285  coexg  5288  funssres  5376  f1oabexg  5604  sefvex  5669  ssimaex  5716  mptfvex  5741  f1ompt  5806  fmptcof  5822  resfunexg  5883  mptexg  5889  funfvima3  5898  ovid  6148  ov  6151  ofres  6259  cofunexg  6280  opabex3d  6292  opabex3  6293  oprabexd  6298  1stcof  6335  2ndcof  6336  mpoexxg  6384  cnvf1o  6399  f2ndf  6400  algrflemg  6404  tposexg  6467  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemi14d  6542  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemres  6571  rdgtfr  6583  rdgruledefgg  6584  rdgon  6595  frecabex  6607  freccllem  6611  frecfcllem  6613  omcl  6672  oeicl  6673  erth  6791  th3qlem1  6849  mapex  6866  pmvalg  6871  mapsnconst  6906  ixpexgg  6934  fundmen  7024  cnvct  7027  snfig  7032  unen  7034  xpdom2  7058  mapxpen  7077  phplem2  7082  findcard2  7121  findcard2s  7122  infnfi  7127  relcnvfi  7183  sbthlemi8  7206  sbthlemi10  7208  fival  7229  fiss  7236  inl11  7324  casef  7347  caseinj  7348  caseinl  7350  caseinr  7351  djudom  7352  difinfsn  7359  djuinj  7365  0ct  7366  ctmlemr  7367  ctssdccl  7370  enomnilem  7397  enmkvlem  7420  enwomnilem  7428  djuassen  7492  xpdjuen  7493  djudoml  7494  djudomr  7495  cc2lem  7545  ltnnnq  7703  nnnq0lem1  7726  addnqprlemfl  7839  addnqprlemfu  7840  mulnqprlemfl  7855  mulnqprlemfu  7856  suplocexprlem2b  7994  prsrlem1  8022  gt0srpr  8028  caucvgsrlemcl  8069  caucvgsrlemfv  8071  caucvgsrlembound  8074  mulcnsr  8115  mulcnsrec  8123  addvalex  8124  pitoregt0  8129  axmulass  8153  axdistr  8154  recriota  8170  mulrid  8236  axmulgt0  8310  cnegexlem2  8414  cnegex  8416  gt0ne0d  8751  recexre  8817  msqge0  8855  mulge0  8858  aptap  8889  recgt0  9089  recreclt  9139  cju  9200  nnge1  9225  nnnlt1  9228  nn0nlt0  9487  nnnle0  9589  elz2  9612  nnm1ge0  9627  recnz  9634  zneo  9642  uz3m2nn  9868  eluz2b2  9898  nn01to3  9912  mnflt  10079  xnn0dcle  10098  xltadd1  10172  lincmb01cmp  10299  iccf1o  10301  fz1n  10341  fseq1p1m1  10391  fznn0  10410  fzctr  10430  4fvwrd4  10437  fzo0n  10465  elfzonlteqm1  10518  divfl0  10619  modqelico  10659  zmodfz  10671  modqid  10674  modqmuladdim  10692  m1modge3gt1  10696  addmodid  10697  frec2uzf1od  10731  frecfzennn  10751  frecfzen2  10752  fzfig  10755  ser0  10858  ser3le  10862  expgt1  10902  expubnd  10921  iexpcyc  10969  binom2sub  10978  binom3  10982  zesq  10983  bernneq  10985  bernneq2  10986  expnbnd  10988  expnlbnd2  10990  facdiv  11063  faclbnd2  11067  faclbnd3  11068  bcval4  11077  hashinfom  11103  hashennn  11105  fihashf1rn  11113  isfinite4im  11117  hashfz  11148  iswrd  11181  iswrdiz  11186  wrdexg  11190  wrdexb  11191  wrdfin  11198  wrdnval  11210  wrdred1hash  11223  ccatsymb  11245  ccatalpha  11256  s111  11274  fzowrddc  11294  swrdlen  11299  swrdwrdsymbg  11311  pfxval  11321  pfx0g  11323  fnpfx  11324  pfxlen  11332  cats1un  11368  swrdccat  11382  crre  11497  crim  11498  remim  11500  mulreap  11504  cjreb  11506  recj  11507  reneg  11508  readd  11509  remullem  11511  imcj  11515  imneg  11516  imadd  11517  cjadd  11524  cjneg  11530  imval2  11534  cjreim  11543  cnrecnv  11550  uzin2  11627  absval  11641  rennim  11642  resqrexlemcalc3  11656  resqrexlemnm  11658  resqrexlemcvg  11659  resqrexlemgt0  11660  resqrexlemga  11663  absreimsq  11707  absreim  11708  amgm2  11758  climconst2  11931  climshft  11944  climshft2  11946  reccn2ap  11953  climge0  11965  sumsnf  12050  sumnul  12065  isumcl  12066  fsum2dlemstep  12075  fisumcom2  12079  fsumabs  12106  fsumiun  12118  binom  12125  bcxmas  12130  arisum  12139  expcnvap0  12143  explecnv  12146  geosergap  12147  geolim  12152  geolim2  12153  geo2sum  12155  geo2lim  12157  cvgratnnlemrate  12171  cvgratz  12173  mertenslemi1  12176  prodf1  12183  prodeq2w  12197  fprodntrivap  12225  prodsnf  12233  fprod2dlemstep  12263  fprodcom2fi  12267  efcllemp  12299  ege2le3  12312  eftlub  12331  efgt1  12338  tanval2ap  12354  tanval3ap  12355  resinval  12356  recosval  12357  efi4p  12358  resin4p  12359  recos4p  12360  resincl  12361  recoscl  12362  efmival  12374  efeul  12375  sinadd  12377  cosadd  12378  tanaddap  12380  sinmul  12385  cos2tsin  12392  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  sin01gt0  12403  cos01gt0  12404  absef  12411  absefib  12412  efieq1re  12413  demoivreALT  12415  eirraplem  12418  3dvds  12505  odd2np1  12514  oddm1even  12516  oddp1even  12517  oexpneg  12518  opoe  12536  omoe  12537  nn0o1gt2  12546  nn0o  12548  bitsdc  12588  bitsfzolem  12595  bitsfzo  12596  bitsinv1lem  12602  bitsinv1  12603  nninfctlemfo  12691  algcvg  12700  algcvgblem  12701  1nprm  12766  1idssfct  12767  oddprmge3  12787  divgcdodd  12795  pw2dvdslemn  12817  pw2dvds  12818  oddpwdclemodd  12824  oddpwdc  12826  phicl2  12866  phibndlem  12868  phibnd  12869  hashdvds  12873  crth  12876  phimullem  12877  eulerthlemfi  12880  eulerthlemrprm  12881  eulerthlema  12882  hashgcdeq  12892  phisum  12893  oddprm  12912  prm23ge5  12917  pythagtriplem1  12918  pythagtriplem4  12921  pythagtriplem12  12928  pythagtriplem14  12930  pczpre  12950  pcadd  12993  pcmpt  12996  pockthlem  13009  pockthi  13011  infpnlem2  13013  gzreim  13032  4sqlem11  13054  4sqlem12  13055  4sqlem13m  13056  4sqlem17  13060  2expltfac  13092  evenennn  13094  ennnfonelemjn  13103  ennnfonelemkh  13113  ennnfonelemhf1o  13114  ennnfonelemex  13115  ennnfonelemhom  13116  ennnfonelemnn0  13123  exmidunben  13127  ctinfomlemom  13128  ssnnctlemct  13147  nninfdc  13154  slotex  13189  setscom  13202  strslfv3  13208  setsslid  13213  bassetsnn  13219  basmex  13222  basmexd  13223  relelbasov  13225  ressbas2d  13231  ressbasid  13233  strressid  13234  ressval3d  13235  2strbas1g  13286  2strop1g  13287  rngbaseg  13299  rngplusgg  13300  rngmulrg  13301  srngbased  13310  srngplusgd  13311  srngmulrd  13312  srnginvld  13313  lmodbased  13328  lmodplusgd  13329  lmodscad  13330  lmodvscad  13331  ipsbased  13340  ipsaddgd  13341  ipsmulrd  13342  ipsscad  13343  ipsvscad  13344  ipsipd  13345  topgrpbasd  13360  topgrpplusgd  13361  topgrptsetd  13362  tgvalex  13426  prdsex  13432  prdsval  13436  prdsbaslemss  13437  prdsbas  13439  prdsplusg  13440  prdsmulr  13441  pwsbas  13455  pwselbasb  13456  pwssnf1o  13461  imasex  13468  imasival  13469  imasbas  13470  imasplusg  13471  imasmulr  13472  imasaddfn  13480  imasaddval  13481  imasaddf  13482  imasmulfn  13483  imasmulval  13484  imasmulf  13485  qusval  13486  qusex  13488  qusaddvallemg  13496  qusaddflemg  13497  qusaddval  13498  qusaddf  13499  qusmulval  13500  qusmulf  13501  xpsfval  13511  xpsval  13515  plusffvalg  13525  grpidvalg  13536  igsumvalx  13552  gsumfzval  13554  gsumress  13558  gsum0g  13559  gsumval2  13560  issubmnd  13605  ress0g  13606  ismhm  13624  mhmex  13625  issubm  13635  0mhm  13649  grppropstrg  13682  grpinvfvalg  13705  grpinvval  13706  grpinvfng  13707  grpsubfvalg  13708  grpsubval  13709  grpressid  13724  grplactfval  13764  qusgrp2  13780  mulgfvalg  13788  mulgex  13790  mulgnngsum  13794  issubg  13840  subgex  13843  subgmulg  13855  issubg2m  13856  releqgg  13887  eqgex  13888  eqgfval  13889  eqgen  13894  isghm  13910  ablressid  14002  mgptopng  14023  rngressid  14048  qusrng  14052  dfur2g  14056  ringidss  14123  ring1  14153  ringressid  14157  qusring2  14160  dvdsrvald  14188  dvdsrex  14193  unitgrp  14211  unitabl  14212  invrfvald  14217  unitlinv  14221  unitrinv  14222  dvrfvald  14228  rdivmuldivd  14239  invrpropdg  14244  rhmunitinv  14273  isnzr2  14279  issubrng  14294  issubrg  14316  subrgugrp  14335  subrgpropd  14348  rrgmex  14356  aprval  14378  islmod  14387  scaffvalg  14402  lssex  14450  lssmex  14451  lsssetm  14452  islssmg  14454  islss3  14475  lspfval  14484  lspval  14486  lspcl  14487  lspex  14491  sralemg  14534  srascag  14538  sravscag  14539  sraipg  14540  sraex  14542  rlmsubg  14554  rlmvnegg  14561  ixpsnbasval  14562  lidlvalg  14567  rspvalg  14568  lidlex  14569  rspex  14570  lidlmex  14571  lidlss  14572  lidlrsppropdg  14591  2idlmex  14597  qusrhm  14624  znlidl  14730  zncrng2  14731  znval  14732  znle  14733  znbaslemnn  14735  znbas  14740  znzrh2  14742  znzrhval  14743  znzrhfo  14744  zndvds  14745  znfi  14751  znhash  14752  znidom  14753  znidomb  14754  psrval  14762  psrbasg  14775  psrelbas  14776  psrplusgg  14779  psraddcl  14781  psr0cl  14782  psrnegcl  14784  psr1clfi  14789  mplvalcoe  14791  mplplusgg  14804  toponsspwpwg  14833  topgele  14840  istps  14843  topontopn  14848  tgclb  14876  lmfval  15004  lmres  15059  ispsmet  15134  psmetge0  15142  ismet  15155  isxmet  15156  xmetge0  15176  isxms2  15263  comet  15310  bdxmet  15312  cnmetdval  15340  cnbl0  15345  cnblcld  15346  reopnap  15357  tgioo  15365  cncfcncntop  15404  cncfmpt2fcntop  15410  maxcncf  15426  mincncf  15427  hovergt0  15461  limcimolemlt  15475  cnplimcim  15478  cnplimclemr  15480  limccnpcntop  15486  limccnp2lem  15487  limccnp2cntop  15488  dvfvalap  15492  dvbss  15496  dvcnp2cntop  15510  dvcn  15511  dvaddxxbr  15512  dvmulxxbr  15513  dvcoapbr  15518  dvcjbr  15519  dvrecap  15524  dvmptfsum  15536  dveflem  15537  plyval  15543  plycolemc  15569  dvply2  15578  reeff1olem  15582  pilem3  15594  ef2kpi  15617  efper  15618  sinperlem  15619  efimpi  15630  ptolemy  15635  sincosq2sgn  15638  sincosq3sgn  15639  sincosq4sgn  15640  sinq12gt0  15641  cosq14gt0  15643  tangtx  15649  sinkpi  15658  coskpi  15659  cosordlem  15660  rplogcl  15690  logge0  15691  logdivlti  15692  logbleb  15772  logblt  15773  binom4  15790  wilthlem1  15794  1sgmprm  15808  1sgm2ppw  15809  mersenne  15811  perfect1  15812  perfectlem1  15813  perfectlem2  15814  perfect  15815  lgsval2lem  15829  lgsval4a  15841  lgsneg  15843  lgsdilem  15846  lgsdirprm  15853  lgsdirnn0  15866  gausslemma2dlem0i  15876  gausslemma2dlem6  15886  gausslemma2dlem7  15887  gausslemma2d  15888  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgsquadlemofi  15895  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  lgsquad2lem2  15901  lgsquad2  15902  m1lgs  15904  2lgs  15923  2lgsoddprmlem2  15925  2lgsoddprm  15932  2sqlem2  15934  vtxvalg  15957  vtxex  15959  struct2slots2dom  15979  structvtxval  15980  structiedg0val  15981  structgrssvtx  15983  structgrssiedg  15984  edgstruct  16005  vdegp1bid  16256  wlkv0  16310  upgr2wlkdc  16318  clwwlkex  16339  clwwlkccatlem  16341  eupthfi  16392  trlsegvdeglem6  16406  konigsberglem1  16429  konigsberglem5  16433  depindlem1  16447  pwf1oexmid  16721  nnnninfex  16748  repiecege0  16759  isomninnlem  16762  iswomninnlem  16782  ismkvnnlem  16785  gfsumsn  16814  gfsump1  16815