Theorem sylancr 414

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancr.1	⊢ 𝜓
sylancr.2	⊢ (𝜑 → 𝜒)
sylancr.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylancr	⊢ (𝜑 → 𝜃)

Proof of Theorem sylancr

Step	Hyp	Ref	Expression
1		sylancr.1	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		sylancr.2	. 2 ⊢ (𝜑 → 𝜒)
4		sylancr.3	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	2, 3, 4	syl2anc 411	1 ⊢ (𝜑 → 𝜃)

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  4178  unipw  4309  opeluu  4547  uniexb  4570  unon  4609  onintrab2im  4616  xpexg  4840  resiexg  5058  imaexg  5090  exse2  5110  soirri  5131  djudisj  5164  elxp5  5225  cnvexg  5274  cnviinm  5278  coexg  5281  funssres  5369  f1oabexg  5595  sefvex  5660  ssimaex  5707  mptfvex  5732  f1ompt  5798  fmptcof  5814  resfunexg  5874  mptexg  5878  funfvima3  5887  ovid  6137  ov  6140  ofres  6249  cofunexg  6270  opabex3d  6282  opabex3  6283  oprabexd  6288  1stcof  6325  2ndcof  6326  mpoexxg  6374  cnvf1o  6389  f2ndf  6390  algrflemg  6394  tposexg  6423  tfrlemisucaccv  6490  tfrlemibxssdm  6492  tfrlemibfn  6493  tfrlemi14d  6498  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemres  6514  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemres  6527  rdgtfr  6539  rdgruledefgg  6540  rdgon  6551  frecabex  6563  freccllem  6567  frecfcllem  6569  omcl  6628  oeicl  6629  erth  6747  th3qlem1  6805  mapex  6822  pmvalg  6827  mapsnconst  6862  ixpexgg  6890  fundmen  6980  cnvct  6983  snfig  6988  unen  6990  xpdom2  7014  mapxpen  7033  phplem2  7038  findcard2  7077  findcard2s  7078  infnfi  7083  relcnvfi  7139  sbthlemi8  7162  sbthlemi10  7164  fival  7168  fiss  7175  inl11  7263  casef  7286  caseinj  7287  caseinl  7289  caseinr  7290  djudom  7291  difinfsn  7298  djuinj  7304  0ct  7305  ctmlemr  7306  ctssdccl  7309  enomnilem  7336  enmkvlem  7359  enwomnilem  7367  djuassen  7431  xpdjuen  7432  djudoml  7433  djudomr  7434  cc2lem  7484  ltnnnq  7642  nnnq0lem1  7665  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemfl  7794  mulnqprlemfu  7795  suplocexprlem2b  7933  prsrlem1  7961  gt0srpr  7967  caucvgsrlemcl  8008  caucvgsrlemfv  8010  caucvgsrlembound  8013  mulcnsr  8054  mulcnsrec  8062  addvalex  8063  pitoregt0  8068  axmulass  8092  axdistr  8093  recriota  8109  mulrid  8175  axmulgt0  8250  cnegexlem2  8354  cnegex  8356  gt0ne0d  8691  recexre  8757  msqge0  8795  mulge0  8798  aptap  8829  recgt0  9029  recreclt  9079  cju  9140  nnge1  9165  nnnlt1  9168  nn0nlt0  9427  nnnle0  9527  elz2  9550  nnm1ge0  9565  recnz  9572  zneo  9580  uz3m2nn  9806  eluz2b2  9836  nn01to3  9850  mnflt  10017  xnn0dcle  10036  xltadd1  10110  lincmb01cmp  10237  iccf1o  10238  fz1n  10278  fseq1p1m1  10328  fznn0  10347  fzctr  10367  4fvwrd4  10374  fzo0n  10402  elfzonlteqm1  10454  divfl0  10555  modqelico  10595  zmodfz  10607  modqid  10610  modqmuladdim  10628  m1modge3gt1  10632  addmodid  10633  frec2uzf1od  10667  frecfzennn  10687  frecfzen2  10688  fzfig  10691  ser0  10794  ser3le  10798  expgt1  10838  expubnd  10857  iexpcyc  10905  binom2sub  10914  binom3  10918  zesq  10919  bernneq  10921  bernneq2  10922  expnbnd  10924  expnlbnd2  10926  facdiv  10999  faclbnd2  11003  faclbnd3  11004  bcval4  11013  hashinfom  11039  hashennn  11041  fihashf1rn  11049  isfinite4im  11053  hashfz  11084  iswrd  11114  iswrdiz  11119  wrdexg  11123  wrdexb  11124  wrdfin  11131  wrdnval  11143  wrdred1hash  11156  ccatsymb  11178  ccatalpha  11189  s111  11207  fzowrddc  11227  swrdlen  11232  swrdwrdsymbg  11244  pfxval  11254  pfx0g  11256  fnpfx  11257  pfxlen  11265  cats1un  11301  swrdccat  11315  crre  11417  crim  11418  remim  11420  mulreap  11424  cjreb  11426  recj  11427  reneg  11428  readd  11429  remullem  11431  imcj  11435  imneg  11436  imadd  11437  cjadd  11444  cjneg  11450  imval2  11454  cjreim  11463  cnrecnv  11470  uzin2  11547  absval  11561  rennim  11562  resqrexlemcalc3  11576  resqrexlemnm  11578  resqrexlemcvg  11579  resqrexlemgt0  11580  resqrexlemga  11583  absreimsq  11627  absreim  11628  amgm2  11678  climconst2  11851  climshft  11864  climshft2  11866  reccn2ap  11873  climge0  11885  sumsnf  11969  sumnul  11984  isumcl  11985  fsum2dlemstep  11994  fisumcom2  11998  fsumabs  12025  fsumiun  12037  binom  12044  bcxmas  12049  arisum  12058  expcnvap0  12062  explecnv  12065  geosergap  12066  geolim  12071  geolim2  12072  geo2sum  12074  geo2lim  12076  cvgratnnlemrate  12090  cvgratz  12092  mertenslemi1  12095  prodf1  12102  prodeq2w  12116  fprodntrivap  12144  prodsnf  12152  fprod2dlemstep  12182  fprodcom2fi  12186  efcllemp  12218  ege2le3  12231  eftlub  12250  efgt1  12257  tanval2ap  12273  tanval3ap  12274  resinval  12275  recosval  12276  efi4p  12277  resin4p  12278  recos4p  12279  resincl  12280  recoscl  12281  efmival  12293  efeul  12294  sinadd  12296  cosadd  12297  tanaddap  12299  sinmul  12304  cos2tsin  12311  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  sin01gt0  12322  cos01gt0  12323  absef  12330  absefib  12331  efieq1re  12332  demoivreALT  12334  eirraplem  12337  3dvds  12424  odd2np1  12433  oddm1even  12435  oddp1even  12436  oexpneg  12437  opoe  12455  omoe  12456  nn0o1gt2  12465  nn0o  12467  bitsdc  12507  bitsfzolem  12514  bitsfzo  12515  bitsinv1lem  12521  bitsinv1  12522  nninfctlemfo  12610  algcvg  12619  algcvgblem  12620  1nprm  12685  1idssfct  12686  oddprmge3  12706  divgcdodd  12714  pw2dvdslemn  12736  pw2dvds  12737  oddpwdclemodd  12743  oddpwdc  12745  phicl2  12785  phibndlem  12787  phibnd  12788  hashdvds  12792  crth  12795  phimullem  12796  eulerthlemfi  12799  eulerthlemrprm  12800  eulerthlema  12801  hashgcdeq  12811  phisum  12812  oddprm  12831  prm23ge5  12836  pythagtriplem1  12837  pythagtriplem4  12840  pythagtriplem12  12847  pythagtriplem14  12849  pczpre  12869  pcadd  12912  pcmpt  12915  pockthlem  12928  pockthi  12930  infpnlem2  12932  gzreim  12951  4sqlem11  12973  4sqlem12  12974  4sqlem13m  12975  4sqlem17  12979  2expltfac  13011  evenennn  13013  ennnfonelemjn  13022  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemnn0  13042  exmidunben  13046  ctinfomlemom  13047  ssnnctlemct  13066  nninfdc  13073  slotex  13108  setscom  13121  strslfv3  13127  setsslid  13132  bassetsnn  13138  basmex  13141  basmexd  13142  relelbasov  13144  ressbas2d  13150  ressbasid  13152  strressid  13153  ressval3d  13154  2strbas1g  13205  2strop1g  13206  rngbaseg  13218  rngplusgg  13219  rngmulrg  13220  srngbased  13229  srngplusgd  13230  srngmulrd  13231  srnginvld  13232  lmodbased  13247  lmodplusgd  13248  lmodscad  13249  lmodvscad  13250  ipsbased  13259  ipsaddgd  13260  ipsmulrd  13261  ipsscad  13262  ipsvscad  13263  ipsipd  13264  topgrpbasd  13279  topgrpplusgd  13280  topgrptsetd  13281  tgvalex  13345  prdsex  13351  prdsval  13355  prdsbaslemss  13356  prdsbas  13358  prdsplusg  13359  prdsmulr  13360  pwsbas  13374  pwselbasb  13375  pwssnf1o  13380  imasex  13387  imasival  13388  imasbas  13389  imasplusg  13390  imasmulr  13391  imasaddfn  13399  imasaddval  13400  imasaddf  13401  imasmulfn  13402  imasmulval  13403  imasmulf  13404  qusval  13405  qusex  13407  qusaddvallemg  13415  qusaddflemg  13416  qusaddval  13417  qusaddf  13418  qusmulval  13419  qusmulf  13420  xpsfval  13430  xpsval  13434  plusffvalg  13444  grpidvalg  13455  igsumvalx  13471  gsumfzval  13473  gsumress  13477  gsum0g  13478  gsumval2  13479  issubmnd  13524  ress0g  13525  ismhm  13543  mhmex  13544  issubm  13554  0mhm  13568  grppropstrg  13601  grpinvfvalg  13624  grpinvval  13625  grpinvfng  13626  grpsubfvalg  13627  grpsubval  13628  grpressid  13643  grplactfval  13683  qusgrp2  13699  mulgfvalg  13707  mulgex  13709  mulgnngsum  13713  issubg  13759  subgex  13762  subgmulg  13774  issubg2m  13775  releqgg  13806  eqgex  13807  eqgfval  13808  eqgen  13813  isghm  13829  ablressid  13921  mgptopng  13941  rngressid  13966  qusrng  13970  dfur2g  13974  ringidss  14041  ring1  14071  ringressid  14075  qusring2  14078  dvdsrvald  14106  dvdsrex  14111  unitgrp  14129  unitabl  14130  invrfvald  14135  unitlinv  14139  unitrinv  14140  dvrfvald  14146  rdivmuldivd  14157  invrpropdg  14162  rhmunitinv  14191  isnzr2  14197  issubrng  14212  issubrg  14234  subrgugrp  14253  subrgpropd  14266  rrgmex  14274  aprval  14295  islmod  14304  scaffvalg  14319  lssex  14367  lssmex  14368  lsssetm  14369  islssmg  14371  islss3  14392  lspfval  14401  lspval  14403  lspcl  14404  lspex  14408  sralemg  14451  srascag  14455  sravscag  14456  sraipg  14457  sraex  14459  rlmsubg  14471  rlmvnegg  14478  ixpsnbasval  14479  lidlvalg  14484  rspvalg  14485  lidlex  14486  rspex  14487  lidlmex  14488  lidlss  14489  lidlrsppropdg  14508  2idlmex  14514  qusrhm  14541  znlidl  14647  zncrng2  14648  znval  14649  znle  14650  znbaslemnn  14652  znbas  14657  znzrh2  14659  znzrhval  14660  znzrhfo  14661  zndvds  14662  znfi  14668  znhash  14669  znidom  14670  znidomb  14671  psrval  14679  psrbasg  14687  psrelbas  14688  psrplusgg  14691  psraddcl  14693  psr0cl  14694  psrnegcl  14696  psr1clfi  14701  mplvalcoe  14703  mplplusgg  14716  toponsspwpwg  14745  topgele  14752  istps  14755  topontopn  14760  tgclb  14788  lmfval  14916  lmres  14971  ispsmet  15046  psmetge0  15054  ismet  15067  isxmet  15068  xmetge0  15088  isxms2  15175  comet  15222  bdxmet  15224  cnmetdval  15252  cnbl0  15257  cnblcld  15258  reopnap  15269  tgioo  15277  cncfcncntop  15316  cncfmpt2fcntop  15322  maxcncf  15338  mincncf  15339  hovergt0  15373  limcimolemlt  15387  cnplimcim  15390  cnplimclemr  15392  limccnpcntop  15398  limccnp2lem  15399  limccnp2cntop  15400  dvfvalap  15404  dvbss  15408  dvcnp2cntop  15422  dvcn  15423  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvrecap  15436  dvmptfsum  15448  dveflem  15449  plyval  15455  plycolemc  15481  dvply2  15490  reeff1olem  15494  pilem3  15506  ef2kpi  15529  efper  15530  sinperlem  15531  efimpi  15542  ptolemy  15547  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  cosq14gt0  15555  tangtx  15561  sinkpi  15570  coskpi  15571  cosordlem  15572  rplogcl  15602  logge0  15603  logdivlti  15604  logbleb  15684  logblt  15685  binom4  15702  wilthlem1  15703  1sgmprm  15717  1sgm2ppw  15718  mersenne  15720  perfect1  15721  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgsval2lem  15738  lgsval4a  15750  lgsneg  15752  lgsdilem  15755  lgsdirprm  15762  lgsdirnn0  15775  gausslemma2dlem0i  15785  gausslemma2dlem6  15795  gausslemma2dlem7  15796  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlemofi  15804  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem2  15810  lgsquad2  15811  m1lgs  15813  2lgs  15832  2lgsoddprmlem2  15834  2lgsoddprm  15841  2sqlem2  15843  vtxvalg  15866  vtxex  15868  struct2slots2dom  15888  structvtxval  15889  structiedg0val  15890  structgrssvtx  15892  structgrssiedg  15893  edgstruct  15914  vdegp1bid  16165  wlkv0  16219  upgr2wlkdc  16227  clwwlkex  16248  clwwlkccatlem  16250  eupthfi  16301  trlsegvdeglem6  16315  pwf1oexmid  16600  nnnninfex  16624  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656