Theorem sylancr 414

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  mpteq2da  4173  unipw  4303  opeluu  4541  uniexb  4564  unon  4603  onintrab2im  4610  xpexg  4833  resiexg  5050  imaexg  5082  exse2  5102  soirri  5123  djudisj  5156  elxp5  5217  cnvexg  5266  cnviinm  5270  coexg  5273  funssres  5360  f1oabexg  5586  sefvex  5650  ssimaex  5697  mptfvex  5722  f1ompt  5788  fmptcof  5804  resfunexg  5864  mptexg  5868  funfvima3  5877  ovid  6127  ov  6130  ofres  6239  cofunexg  6260  opabex3d  6272  opabex3  6273  oprabexd  6278  1stcof  6315  2ndcof  6316  mpoexxg  6362  cnvf1o  6377  f2ndf  6378  algrflemg  6382  tposexg  6410  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemi14d  6485  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemres  6514  rdgtfr  6526  rdgruledefgg  6527  rdgon  6538  frecabex  6550  freccllem  6554  frecfcllem  6556  omcl  6615  oeicl  6616  erth  6734  th3qlem1  6792  mapex  6809  pmvalg  6814  mapsnconst  6849  ixpexgg  6877  fundmen  6967  cnvct  6970  snfig  6975  unen  6977  xpdom2  6998  mapxpen  7017  phplem2  7022  findcard2  7059  findcard2s  7060  infnfi  7065  relcnvfi  7119  sbthlemi8  7142  sbthlemi10  7144  fival  7148  fiss  7155  inl11  7243  casef  7266  caseinj  7267  caseinl  7269  caseinr  7270  djudom  7271  difinfsn  7278  djuinj  7284  0ct  7285  ctmlemr  7286  ctssdccl  7289  enomnilem  7316  enmkvlem  7339  enwomnilem  7347  djuassen  7410  xpdjuen  7411  djudoml  7412  djudomr  7413  cc2lem  7463  ltnnnq  7621  nnnq0lem1  7644  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemfl  7773  mulnqprlemfu  7774  suplocexprlem2b  7912  prsrlem1  7940  gt0srpr  7946  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsrlembound  7992  mulcnsr  8033  mulcnsrec  8041  addvalex  8042  pitoregt0  8047  axmulass  8071  axdistr  8072  recriota  8088  mulrid  8154  axmulgt0  8229  cnegexlem2  8333  cnegex  8335  gt0ne0d  8670  recexre  8736  msqge0  8774  mulge0  8777  aptap  8808  recgt0  9008  recreclt  9058  cju  9119  nnge1  9144  nnnlt1  9147  nn0nlt0  9406  nnnle0  9506  elz2  9529  nnm1ge0  9544  recnz  9551  zneo  9559  uz3m2nn  9780  eluz2b2  9810  nn01to3  9824  mnflt  9991  xnn0dcle  10010  xltadd1  10084  lincmb01cmp  10211  iccf1o  10212  fz1n  10252  fseq1p1m1  10302  fznn0  10321  fzctr  10341  4fvwrd4  10348  fzo0n  10376  elfzonlteqm1  10428  divfl0  10528  modqelico  10568  zmodfz  10580  modqid  10583  modqmuladdim  10601  m1modge3gt1  10605  addmodid  10606  frec2uzf1od  10640  frecfzennn  10660  frecfzen2  10661  fzfig  10664  ser0  10767  ser3le  10771  expgt1  10811  expubnd  10830  iexpcyc  10878  binom2sub  10887  binom3  10891  zesq  10892  bernneq  10894  bernneq2  10895  expnbnd  10897  expnlbnd2  10899  facdiv  10972  faclbnd2  10976  faclbnd3  10977  bcval4  10986  hashinfom  11012  hashennn  11014  fihashf1rn  11022  isfinite4im  11026  hashfz  11056  iswrd  11086  iswrdiz  11091  wrdexg  11095  wrdexb  11096  wrdfin  11103  wrdnval  11115  wrdred1hash  11128  ccatsymb  11150  ccatalpha  11161  s111  11179  fzowrddc  11195  swrdlen  11200  swrdwrdsymbg  11212  pfxval  11222  pfx0g  11224  fnpfx  11225  pfxlen  11233  cats1un  11269  swrdccat  11283  crre  11384  crim  11385  remim  11387  mulreap  11391  cjreb  11393  recj  11394  reneg  11395  readd  11396  remullem  11398  imcj  11402  imneg  11403  imadd  11404  cjadd  11411  cjneg  11417  imval2  11421  cjreim  11430  cnrecnv  11437  uzin2  11514  absval  11528  rennim  11529  resqrexlemcalc3  11543  resqrexlemnm  11545  resqrexlemcvg  11546  resqrexlemgt0  11547  resqrexlemga  11550  absreimsq  11594  absreim  11595  amgm2  11645  climconst2  11818  climshft  11831  climshft2  11833  reccn2ap  11840  climge0  11852  sumsnf  11936  sumnul  11951  isumcl  11952  fsum2dlemstep  11961  fisumcom2  11965  fsumabs  11992  fsumiun  12004  binom  12011  bcxmas  12016  arisum  12025  expcnvap0  12029  explecnv  12032  geosergap  12033  geolim  12038  geolim2  12039  geo2sum  12041  geo2lim  12043  cvgratnnlemrate  12057  cvgratz  12059  mertenslemi1  12062  prodf1  12069  prodeq2w  12083  fprodntrivap  12111  prodsnf  12119  fprod2dlemstep  12149  fprodcom2fi  12153  efcllemp  12185  ege2le3  12198  eftlub  12217  efgt1  12224  tanval2ap  12240  tanval3ap  12241  resinval  12242  recosval  12243  efi4p  12244  resin4p  12245  recos4p  12246  resincl  12247  recoscl  12248  efmival  12260  efeul  12261  sinadd  12263  cosadd  12264  tanaddap  12266  sinmul  12271  cos2tsin  12278  ef01bndlem  12283  sin01bnd  12284  cos01bnd  12285  sin01gt0  12289  cos01gt0  12290  absef  12297  absefib  12298  efieq1re  12299  demoivreALT  12301  eirraplem  12304  3dvds  12391  odd2np1  12400  oddm1even  12402  oddp1even  12403  oexpneg  12404  opoe  12422  omoe  12423  nn0o1gt2  12432  nn0o  12434  bitsdc  12474  bitsfzolem  12481  bitsfzo  12482  bitsinv1lem  12488  bitsinv1  12489  nninfctlemfo  12577  algcvg  12586  algcvgblem  12587  1nprm  12652  1idssfct  12653  oddprmge3  12673  divgcdodd  12681  pw2dvdslemn  12703  pw2dvds  12704  oddpwdclemodd  12710  oddpwdc  12712  phicl2  12752  phibndlem  12754  phibnd  12755  hashdvds  12759  crth  12762  phimullem  12763  eulerthlemfi  12766  eulerthlemrprm  12767  eulerthlema  12768  hashgcdeq  12778  phisum  12779  oddprm  12798  prm23ge5  12803  pythagtriplem1  12804  pythagtriplem4  12807  pythagtriplem12  12814  pythagtriplem14  12816  pczpre  12836  pcadd  12879  pcmpt  12882  pockthlem  12895  pockthi  12897  infpnlem2  12899  gzreim  12918  4sqlem11  12940  4sqlem12  12941  4sqlem13m  12942  4sqlem17  12946  2expltfac  12978  evenennn  12980  ennnfonelemjn  12989  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemnn0  13009  exmidunben  13013  ctinfomlemom  13014  ssnnctlemct  13033  nninfdc  13040  slotex  13075  setscom  13088  strslfv3  13094  setsslid  13099  bassetsnn  13105  basmex  13108  basmexd  13109  relelbasov  13111  ressbas2d  13117  ressbasid  13119  strressid  13120  ressval3d  13121  2strbas1g  13172  2strop1g  13173  rngbaseg  13185  rngplusgg  13186  rngmulrg  13187  srngbased  13196  srngplusgd  13197  srngmulrd  13198  srnginvld  13199  lmodbased  13214  lmodplusgd  13215  lmodscad  13216  lmodvscad  13217  ipsbased  13226  ipsaddgd  13227  ipsmulrd  13228  ipsscad  13229  ipsvscad  13230  ipsipd  13231  topgrpbasd  13246  topgrpplusgd  13247  topgrptsetd  13248  tgvalex  13312  prdsex  13318  prdsval  13322  prdsbaslemss  13323  prdsbas  13325  prdsplusg  13326  prdsmulr  13327  pwsbas  13341  pwselbasb  13342  pwssnf1o  13347  imasex  13354  imasival  13355  imasbas  13356  imasplusg  13357  imasmulr  13358  imasaddfn  13366  imasaddval  13367  imasaddf  13368  imasmulfn  13369  imasmulval  13370  imasmulf  13371  qusval  13372  qusex  13374  qusaddvallemg  13382  qusaddflemg  13383  qusaddval  13384  qusaddf  13385  qusmulval  13386  qusmulf  13387  xpsfval  13397  xpsval  13401  plusffvalg  13411  grpidvalg  13422  igsumvalx  13438  gsumfzval  13440  gsumress  13444  gsum0g  13445  gsumval2  13446  issubmnd  13491  ress0g  13492  ismhm  13510  mhmex  13511  issubm  13521  0mhm  13535  grppropstrg  13568  grpinvfvalg  13591  grpinvval  13592  grpinvfng  13593  grpsubfvalg  13594  grpsubval  13595  grpressid  13610  grplactfval  13650  qusgrp2  13666  mulgfvalg  13674  mulgex  13676  mulgnngsum  13680  issubg  13726  subgex  13729  subgmulg  13741  issubg2m  13742  releqgg  13773  eqgex  13774  eqgfval  13775  eqgen  13780  isghm  13796  ablressid  13888  mgptopng  13908  rngressid  13933  qusrng  13937  dfur2g  13941  ringidss  14008  ring1  14038  ringressid  14042  qusring2  14045  dvdsrvald  14073  dvdsrex  14078  unitgrp  14096  unitabl  14097  invrfvald  14102  unitlinv  14106  unitrinv  14107  dvrfvald  14113  rdivmuldivd  14124  invrpropdg  14129  rhmunitinv  14158  isnzr2  14164  issubrng  14179  issubrg  14201  subrgugrp  14220  subrgpropd  14233  rrgmex  14241  aprval  14262  islmod  14271  scaffvalg  14286  lssex  14334  lssmex  14335  lsssetm  14336  islssmg  14338  islss3  14359  lspfval  14368  lspval  14370  lspcl  14371  lspex  14375  sralemg  14418  srascag  14422  sravscag  14423  sraipg  14424  sraex  14426  rlmsubg  14438  rlmvnegg  14445  ixpsnbasval  14446  lidlvalg  14451  rspvalg  14452  lidlex  14453  rspex  14454  lidlmex  14455  lidlss  14456  lidlrsppropdg  14475  2idlmex  14481  qusrhm  14508  znlidl  14614  zncrng2  14615  znval  14616  znle  14617  znbaslemnn  14619  znbas  14624  znzrh2  14626  znzrhval  14627  znzrhfo  14628  zndvds  14629  znfi  14635  znhash  14636  znidom  14637  znidomb  14638  psrval  14646  psrbasg  14654  psrelbas  14655  psrplusgg  14658  psraddcl  14660  psr0cl  14661  psrnegcl  14663  psr1clfi  14668  mplvalcoe  14670  mplplusgg  14683  toponsspwpwg  14712  topgele  14719  istps  14722  topontopn  14727  tgclb  14755  lmfval  14883  lmres  14938  ispsmet  15013  psmetge0  15021  ismet  15034  isxmet  15035  xmetge0  15055  isxms2  15142  comet  15189  bdxmet  15191  cnmetdval  15219  cnbl0  15224  cnblcld  15225  reopnap  15236  tgioo  15244  cncfcncntop  15283  cncfmpt2fcntop  15289  maxcncf  15305  mincncf  15306  hovergt0  15340  limcimolemlt  15354  cnplimcim  15357  cnplimclemr  15359  limccnpcntop  15365  limccnp2lem  15366  limccnp2cntop  15367  dvfvalap  15371  dvbss  15375  dvcnp2cntop  15389  dvcn  15390  dvaddxxbr  15391  dvmulxxbr  15392  dvcoapbr  15397  dvcjbr  15398  dvrecap  15403  dvmptfsum  15415  dveflem  15416  plyval  15422  plycolemc  15448  dvply2  15457  reeff1olem  15461  pilem3  15473  ef2kpi  15496  efper  15497  sinperlem  15498  efimpi  15509  ptolemy  15514  sincosq2sgn  15517  sincosq3sgn  15518  sincosq4sgn  15519  sinq12gt0  15520  cosq14gt0  15522  tangtx  15528  sinkpi  15537  coskpi  15538  cosordlem  15539  rplogcl  15569  logge0  15570  logdivlti  15571  logbleb  15651  logblt  15652  binom4  15669  wilthlem1  15670  1sgmprm  15684  1sgm2ppw  15685  mersenne  15687  perfect1  15688  perfectlem1  15689  perfectlem2  15690  perfect  15691  lgsval2lem  15705  lgsval4a  15717  lgsneg  15719  lgsdilem  15722  lgsdirprm  15729  lgsdirnn0  15742  gausslemma2dlem0i  15752  gausslemma2dlem6  15762  gausslemma2dlem7  15763  gausslemma2d  15764  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgsquadlemofi  15771  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad2lem2  15777  lgsquad2  15778  m1lgs  15780  2lgs  15799  2lgsoddprmlem2  15801  2lgsoddprm  15808  2sqlem2  15810  vtxvalg  15833  vtxex  15835  struct2slots2dom  15855  structvtxval  15856  structiedg0val  15857  structgrssvtx  15859  structgrssiedg  15860  edgstruct  15880  wlkv0  16115  upgr2wlkdc  16121  clwwlkex  16141  clwwlkccatlem  16143  pwf1oexmid  16452  nnnninfex  16476  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508