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  4071  unipw  4195  opeluu  4428  uniexb  4451  unon  4488  onintrab2im  4495  xpexg  4718  resiexg  4929  imaexg  4958  exse2  4978  soirri  4998  djudisj  5031  elxp5  5092  cnvexg  5141  cnviinm  5145  coexg  5148  funssres  5230  f1oabexg  5444  sefvex  5507  ssimaex  5547  mptfvex  5571  f1ompt  5636  fmptcof  5652  resfunexg  5706  mptexg  5710  funfvima3  5718  ovid  5958  ov  5961  ofres  6064  cofunexg  6077  opabex3d  6089  opabex3  6090  oprabexd  6095  1stcof  6131  2ndcof  6132  mpoexxg  6178  cnvf1o  6193  f2ndf  6194  algrflemg  6198  tposexg  6226  tfrlemisucaccv  6293  tfrlemibxssdm  6295  tfrlemibfn  6296  tfrlemi14d  6301  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemres  6317  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemres  6330  rdgtfr  6342  rdgruledefgg  6343  rdgon  6354  frecabex  6366  freccllem  6370  frecfcllem  6372  omcl  6429  oeicl  6430  erth  6545  th3qlem1  6603  mapex  6620  pmvalg  6625  mapsnconst  6660  ixpexgg  6688  fundmen  6772  cnvct  6775  snfig  6780  unen  6782  xpdom2  6797  mapxpen  6814  phplem2  6819  findcard2  6855  findcard2s  6856  infnfi  6861  relcnvfi  6906  sbthlemi8  6929  sbthlemi10  6931  fival  6935  fiss  6942  inl11  7030  casef  7053  caseinj  7054  caseinl  7056  caseinr  7057  djudom  7058  difinfsn  7065  djuinj  7071  0ct  7072  ctmlemr  7073  ctssdccl  7076  enomnilem  7102  enmkvlem  7125  enwomnilem  7133  djuassen  7173  xpdjuen  7174  djudoml  7175  djudomr  7176  cc2lem  7207  ltnnnq  7364  nnnq0lem1  7387  addnqprlemfl  7500  addnqprlemfu  7501  mulnqprlemfl  7516  mulnqprlemfu  7517  suplocexprlem2b  7655  prsrlem1  7683  gt0srpr  7689  caucvgsrlemcl  7730  caucvgsrlemfv  7732  caucvgsrlembound  7735  mulcnsr  7776  mulcnsrec  7784  addvalex  7785  pitoregt0  7790  axmulass  7814  axdistr  7815  recriota  7831  mulid1  7896  axmulgt0  7970  cnegexlem2  8074  cnegex  8076  gt0ne0d  8410  recexre  8476  msqge0  8514  mulge0  8517  recgt0  8745  recreclt  8795  cju  8856  nnge1  8880  nnnlt1  8883  nn0nlt0  9140  elz2  9262  nnm1ge0  9277  recnz  9284  zneo  9292  uz3m2nn  9511  eluz2b2  9541  nn01to3  9555  mnflt  9719  xnn0dcle  9738  xltadd1  9812  lincmb01cmp  9939  iccf1o  9940  fz1n  9979  fseq1p1m1  10029  fznn0  10048  fzctr  10068  4fvwrd4  10075  elfzonlteqm1  10145  divfl0  10231  modqelico  10269  zmodfz  10281  modqid  10284  modqmuladdim  10302  m1modge3gt1  10306  addmodid  10307  frec2uzf1od  10341  frecfzennn  10361  frecfzen2  10362  fzfig  10365  ser0  10449  ser3le  10453  expgt1  10493  expubnd  10512  iexpcyc  10559  binom2sub  10568  binom3  10572  zesq  10573  bernneq  10575  bernneq2  10576  expnbnd  10578  expnlbnd2  10580  facdiv  10651  faclbnd2  10655  faclbnd3  10656  bcval4  10665  hashinfom  10691  hashennn  10693  fihashf1rn  10702  isfinite4im  10706  hashfz  10734  crre  10799  crim  10800  remim  10802  mulreap  10806  cjreb  10808  recj  10809  reneg  10810  readd  10811  remullem  10813  imcj  10817  imneg  10818  imadd  10819  cjadd  10826  cjneg  10832  imval2  10836  cjreim  10845  cnrecnv  10852  uzin2  10929  absval  10943  rennim  10944  resqrexlemcalc3  10958  resqrexlemnm  10960  resqrexlemcvg  10961  resqrexlemgt0  10962  resqrexlemga  10965  absreimsq  11009  absreim  11010  amgm2  11060  climconst2  11232  climshft  11245  climshft2  11247  reccn2ap  11254  climge0  11266  sumsnf  11350  sumnul  11365  isumcl  11366  fsum2dlemstep  11375  fisumcom2  11379  fsumabs  11406  fsumiun  11418  binom  11425  bcxmas  11430  arisum  11439  expcnvap0  11443  explecnv  11446  geosergap  11447  geolim  11452  geolim2  11453  geo2sum  11455  geo2lim  11457  cvgratnnlemrate  11471  cvgratz  11473  mertenslemi1  11476  prodf1  11483  prodeq2w  11497  fprodntrivap  11525  prodsnf  11533  fprod2dlemstep  11563  fprodcom2fi  11567  efcllemp  11599  ege2le3  11612  eftlub  11631  efgt1  11638  tanval2ap  11654  tanval3ap  11655  resinval  11656  recosval  11657  efi4p  11658  resin4p  11659  recos4p  11660  resincl  11661  recoscl  11662  efmival  11674  efeul  11675  sinadd  11677  cosadd  11678  tanaddap  11680  sinmul  11685  cos2tsin  11692  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  sin01gt0  11702  cos01gt0  11703  absef  11710  absefib  11711  efieq1re  11712  demoivreALT  11714  eirraplem  11717  odd2np1  11810  oddm1even  11812  oddp1even  11813  oexpneg  11814  opoe  11832  omoe  11833  nn0o1gt2  11842  nn0o  11844  algcvg  11980  algcvgblem  11981  1nprm  12046  1idssfct  12047  oddprmge3  12067  divgcdodd  12075  pw2dvdslemn  12097  pw2dvds  12098  oddpwdclemodd  12104  oddpwdc  12106  phicl2  12146  phibndlem  12148  phibnd  12149  hashdvds  12153  crth  12156  phimullem  12157  eulerthlemfi  12160  eulerthlemrprm  12161  eulerthlema  12162  hashgcdeq  12171  phisum  12172  oddprm  12191  prm23ge5  12196  pythagtriplem1  12197  pythagtriplem4  12200  pythagtriplem12  12207  pythagtriplem14  12209  pczpre  12229  pcadd  12271  pcmpt  12273  pockthlem  12286  pockthi  12288  infpnlem2  12290  gzreim  12309  evenennn  12326  ennnfonelemj0  12334  ennnfonelemjn  12335  ennnfonelemg  12336  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemnn0  12355  exmidunben  12359  ctinfomlemom  12360  ssnnctlemct  12379  nninfdc  12386  slotex  12421  setscom  12434  setsslid  12444  basmex  12452  2strbas1g  12499  2strop1g  12500  rngbaseg  12511  rngplusgg  12512  rngmulrg  12513  srngbased  12518  srngplusgd  12519  srngmulrd  12520  srnginvld  12521  lmodbased  12529  lmodplusgd  12530  lmodscad  12531  lmodvscad  12532  ipsbased  12537  ipsaddgd  12538  ipsmulrd  12539  ipsscad  12540  ipsvscad  12541  ipsipd  12542  topgrpbasd  12547  topgrpplusgd  12548  topgrptsetd  12549  plusffvalg  12593  grpidvalg  12604  toponsspwpwg  12670  topgele  12677  istps  12680  topontopn  12685  tgvalex  12700  tgclb  12715  lmfval  12842  lmres  12898  ispsmet  12973  psmetge0  12981  ismet  12994  isxmet  12995  xmetge0  13015  isxms2  13102  comet  13149  bdxmet  13151  cnmetdval  13179  cnbl0  13184  cnblcld  13185  reopnap  13188  tgioo  13196  cncfcncntop  13230  cncfmpt2fcntop  13235  limcimolemlt  13283  cnplimcim  13286  cnplimclemr  13288  limccnpcntop  13294  limccnp2lem  13295  limccnp2cntop  13296  dvfvalap  13300  dvbss  13304  dvcnp2cntop  13313  dvcn  13314  dvaddxxbr  13315  dvmulxxbr  13316  dvcoapbr  13321  dvcjbr  13322  dvrecap  13327  dveflem  13337  reeff1olem  13342  pilem3  13354  ef2kpi  13377  efper  13378  sinperlem  13379  efimpi  13390  ptolemy  13395  sincosq2sgn  13398  sincosq3sgn  13399  sincosq4sgn  13400  sinq12gt0  13401  cosq14gt0  13403  tangtx  13409  sinkpi  13418  coskpi  13419  cosordlem  13420  rplogcl  13450  logge0  13451  logdivlti  13452  logbleb  13529  logblt  13530  binom4  13547  lgsval2lem  13561  lgsval4a  13573  lgsneg  13575  lgsdilem  13578  lgsdirprm  13585  lgsdirnn0  13598  2sqlem2  13601  pwf1oexmid  13889  isomninnlem  13919  iswomninnlem  13938  ismkvnnlem  13941