Theorem sylancr 418

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpteq2da  4220  unipw  4357  opeluu  4596  uniexb  4619  unon  4658  onintrab2im  4665  xpexg  4889  resiexg  5108  imaexg  5140  exse2  5161  soirri  5182  djudisj  5215  elxp5  5276  cnvexg  5325  cnviinm  5329  coexg  5332  funssres  5420  f1oabexg  5651  sefvex  5716  ssimaex  5764  mptfvex  5791  f1ompt  5859  fmptcof  5875  resfunexg  5936  mptexg  5942  funfvima3  5952  ovid  6205  ov  6208  ofres  6317  cofunexg  6338  opabex3d  6350  opabex3  6351  oprabexd  6360  1stcof  6397  2ndcof  6398  mpoexxg  6446  cnvf1o  6461  f2ndf  6462  algrflemg  6466  tposexg  6529  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi14d  6604  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemres  6633  rdgtfr  6645  rdgruledefgg  6646  rdgon  6657  frecabex  6669  freccllem  6673  frecfcllem  6675  omcl  6734  oeicl  6735  erth  6853  th3qlem1  6911  mapex  6928  pmvalg  6933  mapfoss  6947  mapsnconst  6976  ixpexgg  7004  fundmen  7094  cnvct  7097  mapsnend  7099  snfig  7103  unen  7105  xpdom2  7129  mapxpen  7148  phplem2  7154  findcard2  7193  findcard2s  7194  infnfi  7199  relcnvfi  7255  sbthlemi8  7281  sbthlemi10  7283  fival  7304  fiss  7311  inl11  7405  casef  7428  caseinj  7429  caseinl  7431  caseinr  7432  djudom  7433  difinfsn  7440  djuinj  7446  0ct  7447  ctmlemr  7448  ctssdccl  7451  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  djuassen  7573  xpdjuen  7574  djudoml  7575  djudomr  7576  cc2lem  7632  ltnnnq  7790  nnnq0lem1  7813  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  suplocexprlem2b  8081  prsrlem1  8109  gt0srpr  8115  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsrlembound  8161  mulcnsr  8202  mulcnsrec  8210  addvalex  8211  pitoregt0  8216  axmulass  8240  axdistr  8241  recriota  8257  mulrid  8323  axmulgt0  8397  cnegexlem2  8503  cnegex  8505  gt0ne0d  8841  recexre  8908  msqge0  8946  mulge0  8949  aptap  8980  recgt0  9182  recreclt  9232  cju  9293  nnge1  9329  nnnlt1  9332  nn0nlt0  9593  nnnle0  9697  elz2  9720  nnm1ge0  9736  recnz  9743  zneo  9751  uz3m2nn  9982  eluz2b2  10012  nn01to3  10026  mnflt  10195  xnn0dcle  10214  xltadd1  10288  lincmb01cmp  10415  iccf1o  10417  fz1n  10458  fseq1p1m1  10511  fznn0  10530  fzctr  10550  4fvwrd4  10557  fzo0n  10585  elfzonlteqm1  10638  divfl0  10744  modqelico  10784  zmodfz  10796  modqid  10799  modqmuladdim  10817  m1modge3gt1  10821  addmodid  10822  frec2uzf1od  10856  frecfzennn  10876  frecfzen2  10877  fzfig  10880  ser0  10983  ser3le  10987  expgt1  11027  expubnd  11046  iexpcyc  11094  binom2sub  11103  binom3  11107  zesq  11109  bernneq  11111  bernneq2  11112  expnbnd  11114  expnlbnd2  11116  facdiv  11190  faclbnd2  11194  faclbnd3  11195  bcval4  11204  hashinfom  11231  hashennn  11233  fihashf1rn  11241  isfinite4im  11245  hashfz  11276  ssenneg  11294  hashf1lem1  11299  hashf1lem2  11300  iswrd  11320  iswrdiz  11325  wrdexg  11329  wrdexb  11330  wrdfin  11337  wrdnval  11349  wrdred1hash  11362  ccatsymb  11384  ccatalpha  11395  s111  11413  fzowrddc  11433  swrdlen  11438  swrdwrdsymbg  11450  pfxval  11460  pfx0g  11462  fnpfx  11463  pfxlen  11471  cats1un  11507  swrdccat  11521  crre  11636  crim  11637  remim  11639  mulreap  11643  cjreb  11645  recj  11646  reneg  11647  readd  11648  remullem  11650  imcj  11654  imneg  11655  imadd  11656  cjadd  11663  cjneg  11669  imval2  11673  cjreim  11683  cnrecnv  11690  uzin2  11767  absval  11781  rennim  11782  resqrexlemcalc3  11796  resqrexlemnm  11798  resqrexlemcvg  11799  resqrexlemgt0  11800  resqrexlemga  11803  absreimsq  11847  absreim  11848  amgm2  11899  climconst2  12073  climshft  12086  climshft2  12088  reccn2ap  12095  climge0  12107  sumsnf  12192  sumnul  12207  isumcl  12208  fsum2dlemstep  12217  fisumcom2  12221  fsumabs  12248  fsumiun  12260  binom  12267  bcxmas  12272  arisum  12281  expcnvap0  12285  explecnv  12288  geosergap  12289  geolim  12294  geolim2  12295  geo2sum  12297  geo2lim  12299  cvgratnnlemrate  12313  cvgratz  12315  mertenslemi1  12318  prodf1  12325  prodeq2w  12339  fprodntrivap  12367  prodsnf  12375  fprod2dlemstep  12405  fprodcom2fi  12409  efcllemp  12441  ege2le3  12454  eftlub  12473  efgt1  12480  tanval2ap  12496  tanval3ap  12497  resinval  12498  recosval  12499  efi4p  12500  resin4p  12501  recos4p  12502  resincl  12503  recoscl  12504  efmival  12516  efeul  12517  sinadd  12519  cosadd  12520  tanaddap  12522  sinmul  12527  cos2tsin  12534  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  sin01gt0  12545  cos01gt0  12546  absef  12553  absefib  12554  efieq1re  12555  demoivreALT  12557  eirraplem  12560  3dvds  12647  odd2np1  12656  oddm1even  12658  oddp1even  12659  oexpneg  12660  opoe  12678  omoe  12679  nn0o1gt2  12688  nn0o  12690  bitsdc  12730  bitsfzolem  12737  bitsfzo  12738  bitsinv1lem  12744  bitsinv1  12745  nninfctlemfo  12833  algcvg  12842  algcvgblem  12843  1nprm  12908  1idssfct  12909  oddprmge3  12930  divgcdodd  12938  phicl2  13012  phibndlem  13014  phibnd  13015  hashdvds  13019  crth  13022  phimullem  13023  eulerthlemfi  13026  eulerthlemrprm  13027  eulerthlema  13028  hashgcdeq  13038  phisum  13039  oddprm  13058  prm23ge5  13063  pythagtriplem1  13064  pythagtriplem4  13067  pythagtriplem12  13074  pythagtriplem14  13076  pczpre  13096  pcadd  13139  pcmpt  13142  pockthlem  13155  pockthi  13157  infpnlem2  13159  gzreim  13178  4sqlem11  13200  4sqlem12  13201  4sqlem13m  13202  4sqlem17  13206  2expltfac  13239  prmlem0  13240  prmlem1  13242  prmlem2  13254  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemefi  13286  ballotfilemodife  13289  ballotfilem4  13290  evenennn  13333  ennnfonelemjn  13342  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemnn0  13362  exmidunben  13366  ctinfomlemom  13367  ssnnctlemct  13386  nninfdc  13393  slotex  13428  setscom  13441  strslfv3  13447  setsslid  13452  bassetsnn  13458  basmex  13461  basmexd  13462  relelbasov  13465  ressbas2d  13471  ressbasid  13473  strressid  13474  ressval3d  13475  2strbas1g  13526  2strop1g  13527  rngbaseg  13539  rngplusgg  13540  rngmulrg  13541  srngbased  13550  srngplusgd  13551  srngmulrd  13552  srnginvld  13553  lmodbased  13568  lmodplusgd  13569  lmodscad  13570  lmodvscad  13571  ipsbased  13580  ipsaddgd  13581  ipsmulrd  13582  ipsscad  13583  ipsvscad  13584  ipsipd  13585  topgrpbasd  13600  topgrpplusgd  13601  topgrptsetd  13602  tgvalex  13666  imasex  13675  imasival  13676  imasbas  13677  imasplusg  13678  imasmulr  13679  imasaddfn  13687  imasaddval  13688  imasaddf  13689  imasmulfn  13690  imasmulval  13691  imasmulf  13692  qusval  13693  qusex  13695  qusaddvallemg  13703  qusaddflemg  13704  qusaddval  13705  qusaddf  13706  qusmulval  13707  qusmulf  13708  xpsfval  13718  plusffvalg  13731  grpidvalg  13742  gzsumvalx  13758  gzsumfzval  13760  gzsumress  13761  gzsum0  13762  gzsumval2  13763  issubmnd  13804  ress0g  13805  ismhm  13817  mhmex  13818  issubm  13828  0mhm  13842  grppropstrg  13873  grpinvfvalg  13896  grpinvval  13897  grpinvfng  13898  grpsubfvalg  13899  grpsubval  13900  grpressid  13915  grplactfval  13955  qusgrp2  13965  mulgfvalg  13973  mulgex  13975  mulgnngzsum  13979  issubg  14025  subgex  14028  subgmulg  14040  issubg2m  14041  releqgg  14072  eqgex  14073  eqgfval  14074  eqgen  14079  isghm  14095  ablressid  14188  gsumsncmn  14205  gsump1  14206  gsummptfidmadd  14210  prdsex  14221  prdsval  14222  prdsbaslemss  14223  prdsbas  14225  prdsplusg  14226  prdsmulr  14227  xpsval  14250  pwsbas  14254  pwselbasb  14255  pwssnf1o  14260  mgptopng  14277  rngressid  14302  qusrng  14306  dfur2g  14315  ringidss  14383  ring1  14413  ringressid  14417  qusring2  14420  opprringb  14435  dvdsrvald  14449  dvdsrex  14454  unitgrp  14472  unitabl  14473  invrfvald  14478  unitlinv  14482  unitrinv  14483  dvrfvald  14489  rdivmuldivd  14500  invrpropdg  14505  rhmunitinv  14534  isnzr2  14540  issubrng  14556  issubrg  14578  subrgugrp  14597  subrgpropd  14610  rrgmex  14618  aprval  14640  aprprop  14650  islmod  14676  scaffvalg  14692  lssex  14740  lssmex  14741  lsssetm  14742  islssmg  14744  islss3  14765  lspfval  14774  lspval  14776  lspcl  14777  lspex  14781  sralemg  14824  srascag  14828  sravscag  14829  sraipg  14830  sraex  14832  rlmsubg  14844  rlmvnegg  14851  ixpsnbasval  14852  lidlvalg  14857  rspvalg  14858  lidlex  14859  rspex  14860  lidlmex  14861  lidlss  14862  lidlrsppropdg  14881  2idlmex  14887  qusrhm  14914  gsumfsum  14972  znlidl  15018  zncrng2  15019  znval  15020  znle  15021  znbaslemnn  15023  znbas  15028  znzrh2  15030  znzrhval  15031  znzrhfo  15032  zndvds  15033  znfi  15039  znhash  15040  znidom  15041  znidomb  15042  aspval  15064  aspsubrg  15067  asclfval  15070  psrval  15099  psrbasg  15114  psrelbas  15115  psrplusgg  15118  psraddcl  15120  psr0cl  15121  psrnegcl  15123  psr1clfi  15128  mplvalcoe  15130  mplplusgg  15143  toponsspwpwg  15172  topgele  15179  istps  15182  topontopn  15187  tgclb  15215  lmfval  15343  lmres  15398  ispsmet  15473  psmetge0  15481  ismet  15494  isxmet  15495  xmetge0  15515  isxms2  15602  comet  15649  bdxmet  15651  cnmetdval  15679  cnbl0  15684  cnblcld  15685  reopnap  15696  tgioo  15704  cncfcncntop  15743  cncfmpt2fcntop  15749  maxcncf  15765  mincncf  15766  hovergt0  15800  limcimolemlt  15814  cnplimcim  15817  cnplimclemr  15819  limccnpcntop  15825  limccnp2lem  15826  limccnp2cntop  15827  dvfvalap  15831  dvbss  15835  dvcnp2cntop  15849  dvcn  15850  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvrecap  15863  dvmptfsum  15875  dveflem  15876  plyval  15882  plycolemc  15908  dvply2  15917  reeff1olem  15921  pilem3  15934  ef2kpi  15957  efper  15958  sinperlem  15959  efimpi  15970  ptolemy  15975  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  cosq14gt0  15983  tangtx  15989  sinkpi  15998  coskpi  15999  cosordlem  16000  rplogcl  16031  logge0  16032  logdivlti  16033  logbleb  16116  logblt  16117  binom4  16138  log2tlbndlog2  16139  log2ublem2  16141  log2ublog2  16143  birthdaylem2  16145  wilthlem1  16151  ppiqsval  16156  ppiprm  16170  ppinprm  16171  ppiqeq0  16182  1sgmprm  16189  1sgm2ppw  16190  ppiublem1  16192  ppiqub  16194  mersenne  16195  perfect1  16196  perfectlem1  16197  perfectlem2  16198  perfect  16199  bcmono  16202  bcmax  16203  bclbnd  16205  bpos1lem  16207  bpos1  16208  bposlem1  16209  bposlem2  16210  bposlem3  16211  bposlem4  16212  bposlem5  16213  lgsval2lem  16227  lgsval4a  16239  lgsneg  16241  lgsdilem  16244  lgsdirprm  16251  lgsdirnn0  16264  gausslemma2dlem0i  16274  gausslemma2dlem6  16284  gausslemma2dlem7  16285  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgsquadlemofi  16293  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem2  16299  lgsquad2  16300  m1lgs  16302  2lgs  16321  2lgsoddprmlem2  16323  2lgsoddprm  16330  2sqlem2  16332  vtxvalg  16355  vtxex  16357  struct2slots2dom  16377  structvtxval  16378  structiedg0val  16379  structgrssvtx  16381  structgrssiedg  16382  edgstruct  16403  vdegp1bid  16654  wlkv0  16708  upgr2wlkdc  16716  clwwlkex  16737  clwwlkccatlem  16739  eupthfi  16790  trlsegvdeglem6  16804  konigsberglem1  16827  konigsberglem5  16831  depindlem1  16845  pwf1oexmid  17127  nnnninfex  17163  repiecege0  17174  isomninnlem  17177  iswomninnlem  17197  ismkvnnlem  17200