Theorem sylancr 410

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 408	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  4012  unipw  4134  opeluu  4366  uniexb  4389  unon  4422  onintrab2im  4429  xpexg  4648  resiexg  4859  imaexg  4888  exse2  4908  soirri  4928  djudisj  4961  elxp5  5022  cnvexg  5071  cnviinm  5075  coexg  5078  funssres  5160  f1oabexg  5372  sefvex  5435  ssimaex  5475  mptfvex  5499  f1ompt  5564  fmptcof  5580  resfunexg  5634  mptexg  5638  funfvima3  5644  ovid  5880  ov  5883  ofres  5989  cofunexg  6002  opabex3d  6012  opabex3  6013  oprabexd  6018  1stcof  6054  2ndcof  6055  mpoexxg  6101  cnvf1o  6115  f2ndf  6116  algrflemg  6120  tposexg  6148  tfrlemisucaccv  6215  tfrlemibxssdm  6217  tfrlemibfn  6218  tfrlemi14d  6223  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemres  6239  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemres  6252  rdgtfr  6264  rdgruledefgg  6265  rdgon  6276  frecabex  6288  freccllem  6292  frecfcllem  6294  omcl  6350  oeicl  6351  erth  6466  th3qlem1  6524  mapex  6541  pmvalg  6546  mapsnconst  6581  ixpexgg  6609  fundmen  6693  cnvct  6696  snfig  6701  unen  6703  xpdom2  6718  mapxpen  6735  phplem2  6740  findcard2  6776  findcard2s  6777  infnfi  6782  relcnvfi  6822  sbthlemi8  6845  sbthlemi10  6847  fival  6851  fiss  6858  inl11  6943  casef  6966  caseinj  6967  caseinl  6969  caseinr  6970  djudom  6971  difinfsn  6978  djuinj  6984  0ct  6985  ctmlemr  6986  ctssdccl  6989  enomnilem  7003  djuassen  7066  xpdjuen  7067  djudoml  7068  djudomr  7069  ltnnnq  7224  nnnq0lem1  7247  addnqprlemfl  7360  addnqprlemfu  7361  mulnqprlemfl  7376  mulnqprlemfu  7377  suplocexprlem2b  7515  prsrlem1  7543  gt0srpr  7549  caucvgsrlemcl  7590  caucvgsrlemfv  7592  caucvgsrlembound  7595  mulcnsr  7636  mulcnsrec  7644  addvalex  7645  pitoregt0  7650  axmulass  7674  axdistr  7675  recriota  7691  mulid1  7756  axmulgt0  7829  cnegexlem2  7931  cnegex  7933  gt0ne0d  8267  recexre  8333  msqge0  8371  mulge0  8374  recgt0  8601  recreclt  8651  cju  8712  nnge1  8736  nnnlt1  8739  nn0nlt0  8996  elz2  9115  nnm1ge0  9130  recnz  9137  zneo  9145  uz3m2nn  9361  eluz2b2  9390  nn01to3  9402  mnflt  9562  xltadd1  9652  lincmb01cmp  9779  iccf1o  9780  fz1n  9817  fseq1p1m1  9867  fznn0  9886  fzctr  9903  4fvwrd4  9910  elfzonlteqm1  9980  divfl0  10062  modqelico  10100  zmodfz  10112  modqid  10115  modqmuladdim  10133  m1modge3gt1  10137  addmodid  10138  frec2uzf1od  10172  frecfzennn  10192  frecfzen2  10193  fzfig  10196  ser0  10280  ser3le  10284  expgt1  10324  expubnd  10343  iexpcyc  10390  binom2sub  10398  binom3  10402  zesq  10403  bernneq  10405  bernneq2  10406  expnbnd  10408  expnlbnd2  10410  facdiv  10477  faclbnd2  10481  faclbnd3  10482  bcval4  10491  hashinfom  10517  hashennn  10519  fihashf1rn  10528  isfinite4im  10532  hashfz  10560  crre  10622  crim  10623  remim  10625  mulreap  10629  cjreb  10631  recj  10632  reneg  10633  readd  10634  remullem  10636  imcj  10640  imneg  10641  imadd  10642  cjadd  10649  cjneg  10655  imval2  10659  cjreim  10668  cnrecnv  10675  uzin2  10752  absval  10766  rennim  10767  resqrexlemcalc3  10781  resqrexlemnm  10783  resqrexlemcvg  10784  resqrexlemgt0  10785  resqrexlemga  10788  absreimsq  10832  absreim  10833  amgm2  10883  climconst2  11053  climshft  11066  climshft2  11068  reccn2ap  11075  climge0  11087  sumsnf  11171  sumnul  11186  isumcl  11187  fsum2dlemstep  11196  fisumcom2  11200  fsumabs  11227  fsumiun  11239  binom  11246  bcxmas  11251  arisum  11260  expcnvap0  11264  explecnv  11267  geosergap  11268  geolim  11273  geolim2  11274  geo2sum  11276  geo2lim  11278  cvgratnnlemrate  11292  cvgratz  11294  mertenslemi1  11297  prodf1  11304  prodeq2w  11318  efcllemp  11353  ege2le3  11366  eftlub  11385  efgt1  11392  tanval2ap  11409  tanval3ap  11410  resinval  11411  recosval  11412  efi4p  11413  resin4p  11414  recos4p  11415  resincl  11416  recoscl  11417  efmival  11429  efeul  11430  sinadd  11432  cosadd  11433  tanaddap  11435  sinmul  11440  cos2tsin  11447  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  sin01gt0  11457  cos01gt0  11458  absef  11465  absefib  11466  efieq1re  11467  demoivreALT  11469  eirraplem  11472  odd2np1  11559  oddm1even  11561  oddp1even  11562  oexpneg  11563  opoe  11581  omoe  11582  nn0o1gt2  11591  nn0o  11593  algcvg  11718  algcvgblem  11719  1nprm  11784  1idssfct  11785  oddprmge3  11804  divgcdodd  11810  pw2dvdslemn  11832  pw2dvds  11833  oddpwdclemodd  11839  oddpwdc  11841  phicl2  11879  phibndlem  11881  phibnd  11882  hashdvds  11886  crth  11889  phimullem  11890  hashgcdeq  11893  evenennn  11895  ennnfonelemj0  11903  ennnfonelemjn  11904  ennnfonelemg  11905  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemex  11916  ennnfonelemhom  11917  ennnfonelemnn0  11924  exmidunben  11928  ctinfomlemom  11929  slotex  11975  setscom  11988  setsslid  11998  2strbas1g  12052  2strop1g  12053  rngbaseg  12064  rngplusgg  12065  rngmulrg  12066  srngbased  12071  srngplusgd  12072  srngmulrd  12073  srnginvld  12074  lmodbased  12082  lmodplusgd  12083  lmodscad  12084  lmodvscad  12085  ipsbased  12090  ipsaddgd  12091  ipsmulrd  12092  ipsscad  12093  ipsvscad  12094  ipsipd  12095  topgrpbasd  12100  topgrpplusgd  12101  topgrptsetd  12102  toponsspwpwg  12178  topgele  12185  istps  12188  topontopn  12193  tgvalex  12208  tgclb  12223  lmfval  12350  lmres  12406  ispsmet  12481  psmetge0  12489  ismet  12502  isxmet  12503  xmetge0  12523  isxms2  12610  comet  12657  bdxmet  12659  cnmetdval  12687  cnbl0  12692  cnblcld  12693  reopnap  12696  tgioo  12704  cncfcncntop  12738  cncfmpt2fcntop  12743  limcimolemlt  12791  cnplimcim  12794  cnplimclemr  12796  limccnpcntop  12802  limccnp2lem  12803  limccnp2cntop  12804  dvfvalap  12808  dvbss  12812  dvcnp2cntop  12821  dvcn  12822  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  dvcjbr  12830  dvrecap  12835  dveflem  12844  pilem3  12853  ef2kpi  12876  efper  12877  sinperlem  12878  efimpi  12889  ptolemy  12894  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899  sinq12gt0  12900  cosq14gt0  12902  tangtx  12908  sinkpi  12917  coskpi  12918  cosordlem  12919  pwf1oexmid  13183  isomninnlem  13214