Theorem sylancr 408

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpteq2da  3957  unipw  4077  opeluu  4309  uniexb  4332  unon  4365  onintrab2im  4372  xpexg  4591  resiexg  4800  imaexg  4829  exse2  4849  soirri  4869  djudisj  4902  elxp5  4963  cnvexg  5012  cnviinm  5016  coexg  5019  funssres  5101  f1oabexg  5313  sefvex  5374  ssimaex  5414  mptfvex  5438  f1ompt  5503  fmptcof  5519  resfunexg  5573  mptexg  5577  funfvima3  5583  ovid  5819  ov  5822  ofres  5927  cofunexg  5940  opabex3d  5950  opabex3  5951  oprabexd  5956  1stcof  5992  2ndcof  5993  mpoexxg  6038  cnvf1o  6052  f2ndf  6053  algrflemg  6057  tposexg  6085  tfrlemisucaccv  6152  tfrlemibxssdm  6154  tfrlemibfn  6155  tfrlemi14d  6160  tfr1onlemsucaccv  6168  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfr1onlemres  6176  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllembfn  6184  tfrcllemres  6189  rdgtfr  6201  rdgruledefgg  6202  rdgon  6213  frecabex  6225  freccllem  6229  frecfcllem  6231  omcl  6287  oeicl  6288  erth  6403  th3qlem1  6461  mapex  6478  pmvalg  6483  mapsnconst  6518  ixpexgg  6546  fundmen  6630  cnvct  6633  snfig  6638  unen  6640  xpdom2  6654  mapxpen  6671  phplem2  6676  findcard2  6712  findcard2s  6713  infnfi  6718  relcnvfi  6757  sbthlemi8  6780  sbthlemi10  6782  inl11  6865  casef  6888  caseinj  6889  caseinl  6891  caseinr  6892  djudom  6893  difinfsn  6900  djuinj  6906  0ct  6907  ctmlemr  6908  ctssdclemr  6911  enomnilem  6922  djuassen  6977  xpdjuen  6978  djudoml  6979  djudomr  6980  ltnnnq  7132  nnnq0lem1  7155  addnqprlemfl  7268  addnqprlemfu  7269  mulnqprlemfl  7284  mulnqprlemfu  7285  prsrlem1  7438  gt0srpr  7444  caucvgsrlemcl  7484  caucvgsrlemfv  7486  caucvgsrlembound  7489  mulcnsr  7522  mulcnsrec  7530  addvalex  7531  pitoregt0  7536  axmulass  7558  axdistr  7559  recriota  7575  mulid1  7635  axmulgt0  7708  cnegexlem2  7809  cnegex  7811  gt0ne0d  8141  recexre  8206  msqge0  8244  mulge0  8247  recgt0  8466  recreclt  8516  cju  8577  nnge1  8601  nnnlt1  8604  nn0nlt0  8855  elz2  8974  nnm1ge0  8989  recnz  8996  zneo  9004  uz3m2nn  9218  eluz2b2  9247  nn01to3  9259  mnflt  9410  xltadd1  9500  lincmb01cmp  9627  iccf1o  9628  fz1n  9665  fseq1p1m1  9715  fznn0  9734  fzctr  9751  4fvwrd4  9758  elfzonlteqm1  9828  divfl0  9910  modqelico  9948  zmodfz  9960  modqid  9963  modqmuladdim  9981  m1modge3gt1  9985  addmodid  9986  frec2uzf1od  10020  frecfzennn  10040  frecfzen2  10041  fzfig  10044  ser0  10128  ser3le  10132  expgt1  10172  expubnd  10191  iexpcyc  10238  binom2sub  10246  binom3  10250  zesq  10251  bernneq  10253  bernneq2  10254  expnbnd  10256  expnlbnd2  10258  facdiv  10325  faclbnd2  10329  faclbnd3  10330  bcval4  10339  hashinfom  10365  hashennn  10367  fihashf1rn  10376  isfinite4im  10380  hashfz  10408  crre  10470  crim  10471  remim  10473  mulreap  10477  cjreb  10479  recj  10480  reneg  10481  readd  10482  remullem  10484  imcj  10488  imneg  10489  imadd  10490  cjadd  10497  cjneg  10503  imval2  10507  cjreim  10516  cnrecnv  10523  uzin2  10599  absval  10613  rennim  10614  resqrexlemcalc3  10628  resqrexlemnm  10630  resqrexlemcvg  10631  resqrexlemgt0  10632  resqrexlemga  10635  absreimsq  10679  absreim  10680  amgm2  10730  climconst2  10899  climshft  10912  climshft2  10914  reccn2ap  10921  climge0  10933  sumsnf  11017  sumnul  11032  isumcl  11033  fsum2dlemstep  11042  fisumcom2  11046  fsumabs  11073  fsumiun  11085  binom  11092  bcxmas  11097  arisum  11106  expcnvap0  11110  explecnv  11113  geosergap  11114  geolim  11119  geolim2  11120  geo2sum  11122  geo2lim  11124  cvgratnnlemrate  11138  cvgratz  11140  mertenslemi1  11143  efcllemp  11162  ege2le3  11175  eftlub  11194  efgt1  11201  tanval2ap  11218  tanval3ap  11219  resinval  11220  recosval  11221  efi4p  11222  resin4p  11223  recos4p  11224  resincl  11225  recoscl  11226  efmival  11238  efeul  11239  sinadd  11241  cosadd  11242  tanaddap  11244  sinmul  11249  cos2tsin  11256  ef01bndlem  11261  sin01bnd  11262  cos01bnd  11263  sin01gt0  11266  cos01gt0  11267  absef  11273  absefib  11274  efieq1re  11275  demoivreALT  11277  eirraplem  11278  odd2np1  11365  oddm1even  11367  oddp1even  11368  oexpneg  11369  opoe  11387  omoe  11388  nn0o1gt2  11397  nn0o  11399  algcvg  11522  algcvgblem  11523  1nprm  11588  1idssfct  11589  oddprmge3  11608  divgcdodd  11614  pw2dvdslemn  11635  pw2dvds  11636  oddpwdclemodd  11642  oddpwdc  11644  phicl2  11682  phibndlem  11684  phibnd  11685  hashdvds  11689  crth  11692  phimullem  11693  hashgcdeq  11696  evenennn  11698  ennnfonelemj0  11706  ennnfonelemjn  11707  ennnfonelemg  11708  ennnfonelemkh  11717  ennnfonelemhf1o  11718  ennnfonelemex  11719  ennnfonelemhom  11720  ennnfonelemnn0  11727  exmidunben  11731  ctinfomlemom  11732  slotex  11768  setscom  11781  setsslid  11791  2strbas1g  11845  2strop1g  11846  rngbaseg  11857  rngplusgg  11858  rngmulrg  11859  srngbased  11864  srngplusgd  11865  srngmulrd  11866  srnginvld  11867  lmodbased  11875  lmodplusgd  11876  lmodscad  11877  lmodvscad  11878  ipsbased  11883  ipsaddgd  11884  ipsmulrd  11885  ipsscad  11886  ipsvscad  11887  ipsipd  11888  topgrpbasd  11893  topgrpplusgd  11894  topgrptsetd  11895  toponsspwpwg  11971  topgele  11978  istps  11981  topontopn  11986  tgvalex  12001  tgclb  12016  lmfval  12143  lmres  12198  ispsmet  12251  psmetge0  12259  ismet  12272  isxmet  12273  xmetge0  12293  isxms2  12380  comet  12427  bdxmet  12429  cnmetdval  12451  cnbl0  12456  cnblcld  12457  tgioo  12465  cncfcncntop  12493  limcimolemlt  12513  cnplimcim  12516  limccnpcntop  12520  dvfvalap  12523  dvbss  12527  pwf1oexmid  12780  isomninnlem  12809