Theorem sylancr 412

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  4078  unipw  4202  opeluu  4435  uniexb  4458  unon  4495  onintrab2im  4502  xpexg  4725  resiexg  4936  imaexg  4965  exse2  4985  soirri  5005  djudisj  5038  elxp5  5099  cnvexg  5148  cnviinm  5152  coexg  5155  funssres  5240  f1oabexg  5454  sefvex  5517  ssimaex  5557  mptfvex  5581  f1ompt  5647  fmptcof  5663  resfunexg  5717  mptexg  5721  funfvima3  5729  ovid  5969  ov  5972  ofres  6075  cofunexg  6088  opabex3d  6100  opabex3  6101  oprabexd  6106  1stcof  6142  2ndcof  6143  mpoexxg  6189  cnvf1o  6204  f2ndf  6205  algrflemg  6209  tposexg  6237  tfrlemisucaccv  6304  tfrlemibxssdm  6306  tfrlemibfn  6307  tfrlemi14d  6312  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemres  6328  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemres  6341  rdgtfr  6353  rdgruledefgg  6354  rdgon  6365  frecabex  6377  freccllem  6381  frecfcllem  6383  omcl  6440  oeicl  6441  erth  6557  th3qlem1  6615  mapex  6632  pmvalg  6637  mapsnconst  6672  ixpexgg  6700  fundmen  6784  cnvct  6787  snfig  6792  unen  6794  xpdom2  6809  mapxpen  6826  phplem2  6831  findcard2  6867  findcard2s  6868  infnfi  6873  relcnvfi  6918  sbthlemi8  6941  sbthlemi10  6943  fival  6947  fiss  6954  inl11  7042  casef  7065  caseinj  7066  caseinl  7068  caseinr  7069  djudom  7070  difinfsn  7077  djuinj  7083  0ct  7084  ctmlemr  7085  ctssdccl  7088  enomnilem  7114  enmkvlem  7137  enwomnilem  7145  djuassen  7194  xpdjuen  7195  djudoml  7196  djudomr  7197  cc2lem  7228  ltnnnq  7385  nnnq0lem1  7408  addnqprlemfl  7521  addnqprlemfu  7522  mulnqprlemfl  7537  mulnqprlemfu  7538  suplocexprlem2b  7676  prsrlem1  7704  gt0srpr  7710  caucvgsrlemcl  7751  caucvgsrlemfv  7753  caucvgsrlembound  7756  mulcnsr  7797  mulcnsrec  7805  addvalex  7806  pitoregt0  7811  axmulass  7835  axdistr  7836  recriota  7852  mulid1  7917  axmulgt0  7991  cnegexlem2  8095  cnegex  8097  gt0ne0d  8431  recexre  8497  msqge0  8535  mulge0  8538  recgt0  8766  recreclt  8816  cju  8877  nnge1  8901  nnnlt1  8904  nn0nlt0  9161  elz2  9283  nnm1ge0  9298  recnz  9305  zneo  9313  uz3m2nn  9532  eluz2b2  9562  nn01to3  9576  mnflt  9740  xnn0dcle  9759  xltadd1  9833  lincmb01cmp  9960  iccf1o  9961  fz1n  10000  fseq1p1m1  10050  fznn0  10069  fzctr  10089  4fvwrd4  10096  elfzonlteqm1  10166  divfl0  10252  modqelico  10290  zmodfz  10302  modqid  10305  modqmuladdim  10323  m1modge3gt1  10327  addmodid  10328  frec2uzf1od  10362  frecfzennn  10382  frecfzen2  10383  fzfig  10386  ser0  10470  ser3le  10474  expgt1  10514  expubnd  10533  iexpcyc  10580  binom2sub  10589  binom3  10593  zesq  10594  bernneq  10596  bernneq2  10597  expnbnd  10599  expnlbnd2  10601  facdiv  10672  faclbnd2  10676  faclbnd3  10677  bcval4  10686  hashinfom  10712  hashennn  10714  fihashf1rn  10723  isfinite4im  10727  hashfz  10756  crre  10821  crim  10822  remim  10824  mulreap  10828  cjreb  10830  recj  10831  reneg  10832  readd  10833  remullem  10835  imcj  10839  imneg  10840  imadd  10841  cjadd  10848  cjneg  10854  imval2  10858  cjreim  10867  cnrecnv  10874  uzin2  10951  absval  10965  rennim  10966  resqrexlemcalc3  10980  resqrexlemnm  10982  resqrexlemcvg  10983  resqrexlemgt0  10984  resqrexlemga  10987  absreimsq  11031  absreim  11032  amgm2  11082  climconst2  11254  climshft  11267  climshft2  11269  reccn2ap  11276  climge0  11288  sumsnf  11372  sumnul  11387  isumcl  11388  fsum2dlemstep  11397  fisumcom2  11401  fsumabs  11428  fsumiun  11440  binom  11447  bcxmas  11452  arisum  11461  expcnvap0  11465  explecnv  11468  geosergap  11469  geolim  11474  geolim2  11475  geo2sum  11477  geo2lim  11479  cvgratnnlemrate  11493  cvgratz  11495  mertenslemi1  11498  prodf1  11505  prodeq2w  11519  fprodntrivap  11547  prodsnf  11555  fprod2dlemstep  11585  fprodcom2fi  11589  efcllemp  11621  ege2le3  11634  eftlub  11653  efgt1  11660  tanval2ap  11676  tanval3ap  11677  resinval  11678  recosval  11679  efi4p  11680  resin4p  11681  recos4p  11682  resincl  11683  recoscl  11684  efmival  11696  efeul  11697  sinadd  11699  cosadd  11700  tanaddap  11702  sinmul  11707  cos2tsin  11714  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  cos01gt0  11725  absef  11732  absefib  11733  efieq1re  11734  demoivreALT  11736  eirraplem  11739  odd2np1  11832  oddm1even  11834  oddp1even  11835  oexpneg  11836  opoe  11854  omoe  11855  nn0o1gt2  11864  nn0o  11866  algcvg  12002  algcvgblem  12003  1nprm  12068  1idssfct  12069  oddprmge3  12089  divgcdodd  12097  pw2dvdslemn  12119  pw2dvds  12120  oddpwdclemodd  12126  oddpwdc  12128  phicl2  12168  phibndlem  12170  phibnd  12171  hashdvds  12175  crth  12178  phimullem  12179  eulerthlemfi  12182  eulerthlemrprm  12183  eulerthlema  12184  hashgcdeq  12193  phisum  12194  oddprm  12213  prm23ge5  12218  pythagtriplem1  12219  pythagtriplem4  12222  pythagtriplem12  12229  pythagtriplem14  12231  pczpre  12251  pcadd  12293  pcmpt  12295  pockthlem  12308  pockthi  12310  infpnlem2  12312  gzreim  12331  evenennn  12348  ennnfonelemj0  12356  ennnfonelemjn  12357  ennnfonelemg  12358  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemnn0  12377  exmidunben  12381  ctinfomlemom  12382  ssnnctlemct  12401  nninfdc  12408  slotex  12443  setscom  12456  setsslid  12466  basmex  12474  basmexd  12475  2strbas1g  12522  2strop1g  12523  rngbaseg  12534  rngplusgg  12535  rngmulrg  12536  srngbased  12541  srngplusgd  12542  srngmulrd  12543  srnginvld  12544  lmodbased  12552  lmodplusgd  12553  lmodscad  12554  lmodvscad  12555  ipsbased  12560  ipsaddgd  12561  ipsmulrd  12562  ipsscad  12563  ipsvscad  12564  ipsipd  12565  topgrpbasd  12570  topgrpplusgd  12571  topgrptsetd  12572  plusffvalg  12616  grpidvalg  12627  ismhm  12685  issubm  12695  0mhm  12704  grpinvfvalg  12745  grpinvval  12746  grpinvfng  12747  grpsubfvalg  12748  grpsubval  12749  toponsspwpwg  12814  topgele  12821  istps  12824  topontopn  12829  tgvalex  12844  tgclb  12859  lmfval  12986  lmres  13042  ispsmet  13117  psmetge0  13125  ismet  13138  isxmet  13139  xmetge0  13159  isxms2  13246  comet  13293  bdxmet  13295  cnmetdval  13323  cnbl0  13328  cnblcld  13329  reopnap  13332  tgioo  13340  cncfcncntop  13374  cncfmpt2fcntop  13379  limcimolemlt  13427  cnplimcim  13430  cnplimclemr  13432  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  dvfvalap  13444  dvbss  13448  dvcnp2cntop  13457  dvcn  13458  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvrecap  13471  dveflem  13481  reeff1olem  13486  pilem3  13498  ef2kpi  13521  efper  13522  sinperlem  13523  efimpi  13534  ptolemy  13539  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  cosq14gt0  13547  tangtx  13553  sinkpi  13562  coskpi  13563  cosordlem  13564  rplogcl  13594  logge0  13595  logdivlti  13596  logbleb  13673  logblt  13674  binom4  13691  lgsval2lem  13705  lgsval4a  13717  lgsneg  13719  lgsdilem  13722  lgsdirprm  13729  lgsdirnn0  13742  2sqlem2  13745  pwf1oexmid  14032  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084