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  4076  unipw  4200  opeluu  4433  uniexb  4456  unon  4493  onintrab2im  4500  xpexg  4723  resiexg  4934  imaexg  4963  exse2  4983  soirri  5003  djudisj  5036  elxp5  5097  cnvexg  5146  cnviinm  5150  coexg  5153  funssres  5238  f1oabexg  5452  sefvex  5515  ssimaex  5555  mptfvex  5579  f1ompt  5644  fmptcof  5660  resfunexg  5714  mptexg  5718  funfvima3  5726  ovid  5966  ov  5969  ofres  6072  cofunexg  6085  opabex3d  6097  opabex3  6098  oprabexd  6103  1stcof  6139  2ndcof  6140  mpoexxg  6186  cnvf1o  6201  f2ndf  6202  algrflemg  6206  tposexg  6234  tfrlemisucaccv  6301  tfrlemibxssdm  6303  tfrlemibfn  6304  tfrlemi14d  6309  tfr1onlemsucaccv  6317  tfr1onlembxssdm  6319  tfr1onlembfn  6320  tfr1onlemres  6325  tfrcllemsucaccv  6330  tfrcllembxssdm  6332  tfrcllembfn  6333  tfrcllemres  6338  rdgtfr  6350  rdgruledefgg  6351  rdgon  6362  frecabex  6374  freccllem  6378  frecfcllem  6380  omcl  6437  oeicl  6438  erth  6553  th3qlem1  6611  mapex  6628  pmvalg  6633  mapsnconst  6668  ixpexgg  6696  fundmen  6780  cnvct  6783  snfig  6788  unen  6790  xpdom2  6805  mapxpen  6822  phplem2  6827  findcard2  6863  findcard2s  6864  infnfi  6869  relcnvfi  6914  sbthlemi8  6937  sbthlemi10  6939  fival  6943  fiss  6950  inl11  7038  casef  7061  caseinj  7062  caseinl  7064  caseinr  7065  djudom  7066  difinfsn  7073  djuinj  7079  0ct  7080  ctmlemr  7081  ctssdccl  7084  enomnilem  7110  enmkvlem  7133  enwomnilem  7141  djuassen  7181  xpdjuen  7182  djudoml  7183  djudomr  7184  cc2lem  7215  ltnnnq  7372  nnnq0lem1  7395  addnqprlemfl  7508  addnqprlemfu  7509  mulnqprlemfl  7524  mulnqprlemfu  7525  suplocexprlem2b  7663  prsrlem1  7691  gt0srpr  7697  caucvgsrlemcl  7738  caucvgsrlemfv  7740  caucvgsrlembound  7743  mulcnsr  7784  mulcnsrec  7792  addvalex  7793  pitoregt0  7798  axmulass  7822  axdistr  7823  recriota  7839  mulid1  7904  axmulgt0  7978  cnegexlem2  8082  cnegex  8084  gt0ne0d  8418  recexre  8484  msqge0  8522  mulge0  8525  recgt0  8753  recreclt  8803  cju  8864  nnge1  8888  nnnlt1  8891  nn0nlt0  9148  elz2  9270  nnm1ge0  9285  recnz  9292  zneo  9300  uz3m2nn  9519  eluz2b2  9549  nn01to3  9563  mnflt  9727  xnn0dcle  9746  xltadd1  9820  lincmb01cmp  9947  iccf1o  9948  fz1n  9987  fseq1p1m1  10037  fznn0  10056  fzctr  10076  4fvwrd4  10083  elfzonlteqm1  10153  divfl0  10239  modqelico  10277  zmodfz  10289  modqid  10292  modqmuladdim  10310  m1modge3gt1  10314  addmodid  10315  frec2uzf1od  10349  frecfzennn  10369  frecfzen2  10370  fzfig  10373  ser0  10457  ser3le  10461  expgt1  10501  expubnd  10520  iexpcyc  10567  binom2sub  10576  binom3  10580  zesq  10581  bernneq  10583  bernneq2  10584  expnbnd  10586  expnlbnd2  10588  facdiv  10659  faclbnd2  10663  faclbnd3  10664  bcval4  10673  hashinfom  10699  hashennn  10701  fihashf1rn  10710  isfinite4im  10714  hashfz  10743  crre  10808  crim  10809  remim  10811  mulreap  10815  cjreb  10817  recj  10818  reneg  10819  readd  10820  remullem  10822  imcj  10826  imneg  10827  imadd  10828  cjadd  10835  cjneg  10841  imval2  10845  cjreim  10854  cnrecnv  10861  uzin2  10938  absval  10952  rennim  10953  resqrexlemcalc3  10967  resqrexlemnm  10969  resqrexlemcvg  10970  resqrexlemgt0  10971  resqrexlemga  10974  absreimsq  11018  absreim  11019  amgm2  11069  climconst2  11241  climshft  11254  climshft2  11256  reccn2ap  11263  climge0  11275  sumsnf  11359  sumnul  11374  isumcl  11375  fsum2dlemstep  11384  fisumcom2  11388  fsumabs  11415  fsumiun  11427  binom  11434  bcxmas  11439  arisum  11448  expcnvap0  11452  explecnv  11455  geosergap  11456  geolim  11461  geolim2  11462  geo2sum  11464  geo2lim  11466  cvgratnnlemrate  11480  cvgratz  11482  mertenslemi1  11485  prodf1  11492  prodeq2w  11506  fprodntrivap  11534  prodsnf  11542  fprod2dlemstep  11572  fprodcom2fi  11576  efcllemp  11608  ege2le3  11621  eftlub  11640  efgt1  11647  tanval2ap  11663  tanval3ap  11664  resinval  11665  recosval  11666  efi4p  11667  resin4p  11668  recos4p  11669  resincl  11670  recoscl  11671  efmival  11683  efeul  11684  sinadd  11686  cosadd  11687  tanaddap  11689  sinmul  11694  cos2tsin  11701  ef01bndlem  11706  sin01bnd  11707  cos01bnd  11708  sin01gt0  11711  cos01gt0  11712  absef  11719  absefib  11720  efieq1re  11721  demoivreALT  11723  eirraplem  11726  odd2np1  11819  oddm1even  11821  oddp1even  11822  oexpneg  11823  opoe  11841  omoe  11842  nn0o1gt2  11851  nn0o  11853  algcvg  11989  algcvgblem  11990  1nprm  12055  1idssfct  12056  oddprmge3  12076  divgcdodd  12084  pw2dvdslemn  12106  pw2dvds  12107  oddpwdclemodd  12113  oddpwdc  12115  phicl2  12155  phibndlem  12157  phibnd  12158  hashdvds  12162  crth  12165  phimullem  12166  eulerthlemfi  12169  eulerthlemrprm  12170  eulerthlema  12171  hashgcdeq  12180  phisum  12181  oddprm  12200  prm23ge5  12205  pythagtriplem1  12206  pythagtriplem4  12209  pythagtriplem12  12216  pythagtriplem14  12218  pczpre  12238  pcadd  12280  pcmpt  12282  pockthlem  12295  pockthi  12297  infpnlem2  12299  gzreim  12318  evenennn  12335  ennnfonelemj0  12343  ennnfonelemjn  12344  ennnfonelemg  12345  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemnn0  12364  exmidunben  12368  ctinfomlemom  12369  ssnnctlemct  12388  nninfdc  12395  slotex  12430  setscom  12443  setsslid  12453  basmex  12461  basmexd  12462  2strbas1g  12509  2strop1g  12510  rngbaseg  12521  rngplusgg  12522  rngmulrg  12523  srngbased  12528  srngplusgd  12529  srngmulrd  12530  srnginvld  12531  lmodbased  12539  lmodplusgd  12540  lmodscad  12541  lmodvscad  12542  ipsbased  12547  ipsaddgd  12548  ipsmulrd  12549  ipsscad  12550  ipsvscad  12551  ipsipd  12552  topgrpbasd  12557  topgrpplusgd  12558  topgrptsetd  12559  plusffvalg  12603  grpidvalg  12614  ismhm  12672  issubm  12682  0mhm  12691  toponsspwpwg  12773  topgele  12780  istps  12783  topontopn  12788  tgvalex  12803  tgclb  12818  lmfval  12945  lmres  13001  ispsmet  13076  psmetge0  13084  ismet  13097  isxmet  13098  xmetge0  13118  isxms2  13205  comet  13252  bdxmet  13254  cnmetdval  13282  cnbl0  13287  cnblcld  13288  reopnap  13291  tgioo  13299  cncfcncntop  13333  cncfmpt2fcntop  13338  limcimolemlt  13386  cnplimcim  13389  cnplimclemr  13391  limccnpcntop  13397  limccnp2lem  13398  limccnp2cntop  13399  dvfvalap  13403  dvbss  13407  dvcnp2cntop  13416  dvcn  13417  dvaddxxbr  13418  dvmulxxbr  13419  dvcoapbr  13424  dvcjbr  13425  dvrecap  13430  dveflem  13440  reeff1olem  13445  pilem3  13457  ef2kpi  13480  efper  13481  sinperlem  13482  efimpi  13493  ptolemy  13498  sincosq2sgn  13501  sincosq3sgn  13502  sincosq4sgn  13503  sinq12gt0  13504  cosq14gt0  13506  tangtx  13512  sinkpi  13521  coskpi  13522  cosordlem  13523  rplogcl  13553  logge0  13554  logdivlti  13555  logbleb  13632  logblt  13633  binom4  13650  lgsval2lem  13664  lgsval4a  13676  lgsneg  13678  lgsdilem  13681  lgsdirprm  13688  lgsdirnn0  13701  2sqlem2  13704  pwf1oexmid  13992  isomninnlem  14022  iswomninnlem  14041  ismkvnnlem  14044