Theorem sylancr 411

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 409	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpteq2da  4065  unipw  4189  opeluu  4422  uniexb  4445  unon  4482  onintrab2im  4489  xpexg  4712  resiexg  4923  imaexg  4952  exse2  4972  soirri  4992  djudisj  5025  elxp5  5086  cnvexg  5135  cnviinm  5139  coexg  5142  funssres  5224  f1oabexg  5438  sefvex  5501  ssimaex  5541  mptfvex  5565  f1ompt  5630  fmptcof  5646  resfunexg  5700  mptexg  5704  funfvima3  5712  ovid  5949  ov  5952  ofres  6058  cofunexg  6071  opabex3d  6081  opabex3  6082  oprabexd  6087  1stcof  6123  2ndcof  6124  mpoexxg  6170  cnvf1o  6184  f2ndf  6185  algrflemg  6189  tposexg  6217  tfrlemisucaccv  6284  tfrlemibxssdm  6286  tfrlemibfn  6287  tfrlemi14d  6292  tfr1onlemsucaccv  6300  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfr1onlemres  6308  tfrcllemsucaccv  6313  tfrcllembxssdm  6315  tfrcllembfn  6316  tfrcllemres  6321  rdgtfr  6333  rdgruledefgg  6334  rdgon  6345  frecabex  6357  freccllem  6361  frecfcllem  6363  omcl  6420  oeicl  6421  erth  6536  th3qlem1  6594  mapex  6611  pmvalg  6616  mapsnconst  6651  ixpexgg  6679  fundmen  6763  cnvct  6766  snfig  6771  unen  6773  xpdom2  6788  mapxpen  6805  phplem2  6810  findcard2  6846  findcard2s  6847  infnfi  6852  relcnvfi  6897  sbthlemi8  6920  sbthlemi10  6922  fival  6926  fiss  6933  inl11  7021  casef  7044  caseinj  7045  caseinl  7047  caseinr  7048  djudom  7049  difinfsn  7056  djuinj  7062  0ct  7063  ctmlemr  7064  ctssdccl  7067  enomnilem  7093  enmkvlem  7116  enwomnilem  7124  djuassen  7164  xpdjuen  7165  djudoml  7166  djudomr  7167  cc2lem  7198  ltnnnq  7355  nnnq0lem1  7378  addnqprlemfl  7491  addnqprlemfu  7492  mulnqprlemfl  7507  mulnqprlemfu  7508  suplocexprlem2b  7646  prsrlem1  7674  gt0srpr  7680  caucvgsrlemcl  7721  caucvgsrlemfv  7723  caucvgsrlembound  7726  mulcnsr  7767  mulcnsrec  7775  addvalex  7776  pitoregt0  7781  axmulass  7805  axdistr  7806  recriota  7822  mulid1  7887  axmulgt0  7961  cnegexlem2  8065  cnegex  8067  gt0ne0d  8401  recexre  8467  msqge0  8505  mulge0  8508  recgt0  8736  recreclt  8786  cju  8847  nnge1  8871  nnnlt1  8874  nn0nlt0  9131  elz2  9253  nnm1ge0  9268  recnz  9275  zneo  9283  uz3m2nn  9502  eluz2b2  9532  nn01to3  9546  mnflt  9710  xnn0dcle  9729  xltadd1  9803  lincmb01cmp  9930  iccf1o  9931  fz1n  9969  fseq1p1m1  10019  fznn0  10038  fzctr  10058  4fvwrd4  10065  elfzonlteqm1  10135  divfl0  10221  modqelico  10259  zmodfz  10271  modqid  10274  modqmuladdim  10292  m1modge3gt1  10296  addmodid  10297  frec2uzf1od  10331  frecfzennn  10351  frecfzen2  10352  fzfig  10355  ser0  10439  ser3le  10443  expgt1  10483  expubnd  10502  iexpcyc  10549  binom2sub  10557  binom3  10561  zesq  10562  bernneq  10564  bernneq2  10565  expnbnd  10567  expnlbnd2  10569  facdiv  10640  faclbnd2  10644  faclbnd3  10645  bcval4  10654  hashinfom  10680  hashennn  10682  fihashf1rn  10691  isfinite4im  10695  hashfz  10723  crre  10785  crim  10786  remim  10788  mulreap  10792  cjreb  10794  recj  10795  reneg  10796  readd  10797  remullem  10799  imcj  10803  imneg  10804  imadd  10805  cjadd  10812  cjneg  10818  imval2  10822  cjreim  10831  cnrecnv  10838  uzin2  10915  absval  10929  rennim  10930  resqrexlemcalc3  10944  resqrexlemnm  10946  resqrexlemcvg  10947  resqrexlemgt0  10948  resqrexlemga  10951  absreimsq  10995  absreim  10996  amgm2  11046  climconst2  11218  climshft  11231  climshft2  11233  reccn2ap  11240  climge0  11252  sumsnf  11336  sumnul  11351  isumcl  11352  fsum2dlemstep  11361  fisumcom2  11365  fsumabs  11392  fsumiun  11404  binom  11411  bcxmas  11416  arisum  11425  expcnvap0  11429  explecnv  11432  geosergap  11433  geolim  11438  geolim2  11439  geo2sum  11441  geo2lim  11443  cvgratnnlemrate  11457  cvgratz  11459  mertenslemi1  11462  prodf1  11469  prodeq2w  11483  fprodntrivap  11511  prodsnf  11519  fprod2dlemstep  11549  fprodcom2fi  11553  efcllemp  11585  ege2le3  11598  eftlub  11617  efgt1  11624  tanval2ap  11640  tanval3ap  11641  resinval  11642  recosval  11643  efi4p  11644  resin4p  11645  recos4p  11646  resincl  11647  recoscl  11648  efmival  11660  efeul  11661  sinadd  11663  cosadd  11664  tanaddap  11666  sinmul  11671  cos2tsin  11678  ef01bndlem  11683  sin01bnd  11684  cos01bnd  11685  sin01gt0  11688  cos01gt0  11689  absef  11696  absefib  11697  efieq1re  11698  demoivreALT  11700  eirraplem  11703  odd2np1  11795  oddm1even  11797  oddp1even  11798  oexpneg  11799  opoe  11817  omoe  11818  nn0o1gt2  11827  nn0o  11829  algcvg  11959  algcvgblem  11960  1nprm  12025  1idssfct  12026  oddprmge3  12046  divgcdodd  12052  pw2dvdslemn  12074  pw2dvds  12075  oddpwdclemodd  12081  oddpwdc  12083  phicl2  12123  phibndlem  12125  phibnd  12126  hashdvds  12130  crth  12133  phimullem  12134  eulerthlemfi  12137  eulerthlemrprm  12138  eulerthlema  12139  hashgcdeq  12148  phisum  12149  oddprm  12168  prm23ge5  12173  pythagtriplem1  12174  pythagtriplem4  12177  pythagtriplem12  12184  pythagtriplem14  12186  pczpre  12206  pcadd  12248  pcmpt  12250  evenennn  12263  ennnfonelemj0  12271  ennnfonelemjn  12272  ennnfonelemg  12273  ennnfonelemkh  12282  ennnfonelemhf1o  12283  ennnfonelemex  12284  ennnfonelemhom  12285  ennnfonelemnn0  12292  exmidunben  12296  ctinfomlemom  12297  ssnnctlemct  12316  nninfdc  12325  slotex  12358  setscom  12371  setsslid  12381  2strbas1g  12435  2strop1g  12436  rngbaseg  12447  rngplusgg  12448  rngmulrg  12449  srngbased  12454  srngplusgd  12455  srngmulrd  12456  srnginvld  12457  lmodbased  12465  lmodplusgd  12466  lmodscad  12467  lmodvscad  12468  ipsbased  12473  ipsaddgd  12474  ipsmulrd  12475  ipsscad  12476  ipsvscad  12477  ipsipd  12478  topgrpbasd  12483  topgrpplusgd  12484  topgrptsetd  12485  toponsspwpwg  12561  topgele  12568  istps  12571  topontopn  12576  tgvalex  12591  tgclb  12606  lmfval  12733  lmres  12789  ispsmet  12864  psmetge0  12872  ismet  12885  isxmet  12886  xmetge0  12906  isxms2  12993  comet  13040  bdxmet  13042  cnmetdval  13070  cnbl0  13075  cnblcld  13076  reopnap  13079  tgioo  13087  cncfcncntop  13121  cncfmpt2fcntop  13126  limcimolemlt  13174  cnplimcim  13177  cnplimclemr  13179  limccnpcntop  13185  limccnp2lem  13186  limccnp2cntop  13187  dvfvalap  13191  dvbss  13195  dvcnp2cntop  13204  dvcn  13205  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvcjbr  13213  dvrecap  13218  dveflem  13228  reeff1olem  13233  pilem3  13245  ef2kpi  13268  efper  13269  sinperlem  13270  efimpi  13281  ptolemy  13286  sincosq2sgn  13289  sincosq3sgn  13290  sincosq4sgn  13291  sinq12gt0  13292  cosq14gt0  13294  tangtx  13300  sinkpi  13309  coskpi  13310  cosordlem  13311  rplogcl  13341  logge0  13342  logdivlti  13343  logbleb  13420  logblt  13421  binom4  13438  pwf1oexmid  13713  isomninnlem  13743  iswomninnlem  13762  ismkvnnlem  13765