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  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  7116  sbthlemi8  7139  sbthlemi10  7141  fival  7145  fiss  7152  inl11  7240  casef  7263  caseinj  7264  caseinl  7266  caseinr  7267  djudom  7268  difinfsn  7275  djuinj  7281  0ct  7282  ctmlemr  7283  ctssdccl  7286  enomnilem  7313  enmkvlem  7336  enwomnilem  7344  djuassen  7407  xpdjuen  7408  djudoml  7409  djudomr  7410  cc2lem  7460  ltnnnq  7618  nnnq0lem1  7641  addnqprlemfl  7754  addnqprlemfu  7755  mulnqprlemfl  7770  mulnqprlemfu  7771  suplocexprlem2b  7909  prsrlem1  7937  gt0srpr  7943  caucvgsrlemcl  7984  caucvgsrlemfv  7986  caucvgsrlembound  7989  mulcnsr  8030  mulcnsrec  8038  addvalex  8039  pitoregt0  8044  axmulass  8068  axdistr  8069  recriota  8085  mulrid  8151  axmulgt0  8226  cnegexlem2  8330  cnegex  8332  gt0ne0d  8667  recexre  8733  msqge0  8771  mulge0  8774  aptap  8805  recgt0  9005  recreclt  9055  cju  9116  nnge1  9141  nnnlt1  9144  nn0nlt0  9403  nnnle0  9503  elz2  9526  nnm1ge0  9541  recnz  9548  zneo  9556  uz3m2nn  9776  eluz2b2  9806  nn01to3  9820  mnflt  9987  xnn0dcle  10006  xltadd1  10080  lincmb01cmp  10207  iccf1o  10208  fz1n  10248  fseq1p1m1  10298  fznn0  10317  fzctr  10337  4fvwrd4  10344  fzo0n  10372  elfzonlteqm1  10424  divfl0  10524  modqelico  10564  zmodfz  10576  modqid  10579  modqmuladdim  10597  m1modge3gt1  10601  addmodid  10602  frec2uzf1od  10636  frecfzennn  10656  frecfzen2  10657  fzfig  10660  ser0  10763  ser3le  10767  expgt1  10807  expubnd  10826  iexpcyc  10874  binom2sub  10883  binom3  10887  zesq  10888  bernneq  10890  bernneq2  10891  expnbnd  10893  expnlbnd2  10895  facdiv  10968  faclbnd2  10972  faclbnd3  10973  bcval4  10982  hashinfom  11008  hashennn  11010  fihashf1rn  11018  isfinite4im  11022  hashfz  11051  iswrd  11081  iswrdiz  11086  wrdexg  11090  wrdexb  11091  wrdfin  11098  wrdnval  11110  wrdred1hash  11123  ccatsymb  11145  s111  11172  fzowrddc  11187  swrdlen  11192  swrdwrdsymbg  11204  pfxval  11214  pfx0g  11216  fnpfx  11217  pfxlen  11225  cats1un  11261  swrdccat  11275  crre  11376  crim  11377  remim  11379  mulreap  11383  cjreb  11385  recj  11386  reneg  11387  readd  11388  remullem  11390  imcj  11394  imneg  11395  imadd  11396  cjadd  11403  cjneg  11409  imval2  11413  cjreim  11422  cnrecnv  11429  uzin2  11506  absval  11520  rennim  11521  resqrexlemcalc3  11535  resqrexlemnm  11537  resqrexlemcvg  11538  resqrexlemgt0  11539  resqrexlemga  11542  absreimsq  11586  absreim  11587  amgm2  11637  climconst2  11810  climshft  11823  climshft2  11825  reccn2ap  11832  climge0  11844  sumsnf  11928  sumnul  11943  isumcl  11944  fsum2dlemstep  11953  fisumcom2  11957  fsumabs  11984  fsumiun  11996  binom  12003  bcxmas  12008  arisum  12017  expcnvap0  12021  explecnv  12024  geosergap  12025  geolim  12030  geolim2  12031  geo2sum  12033  geo2lim  12035  cvgratnnlemrate  12049  cvgratz  12051  mertenslemi1  12054  prodf1  12061  prodeq2w  12075  fprodntrivap  12103  prodsnf  12111  fprod2dlemstep  12141  fprodcom2fi  12145  efcllemp  12177  ege2le3  12190  eftlub  12209  efgt1  12216  tanval2ap  12232  tanval3ap  12233  resinval  12234  recosval  12235  efi4p  12236  resin4p  12237  recos4p  12238  resincl  12239  recoscl  12240  efmival  12252  efeul  12253  sinadd  12255  cosadd  12256  tanaddap  12258  sinmul  12263  cos2tsin  12270  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  sin01gt0  12281  cos01gt0  12282  absef  12289  absefib  12290  efieq1re  12291  demoivreALT  12293  eirraplem  12296  3dvds  12383  odd2np1  12392  oddm1even  12394  oddp1even  12395  oexpneg  12396  opoe  12414  omoe  12415  nn0o1gt2  12424  nn0o  12426  bitsdc  12466  bitsfzolem  12473  bitsfzo  12474  bitsinv1lem  12480  bitsinv1  12481  nninfctlemfo  12569  algcvg  12578  algcvgblem  12579  1nprm  12644  1idssfct  12645  oddprmge3  12665  divgcdodd  12673  pw2dvdslemn  12695  pw2dvds  12696  oddpwdclemodd  12702  oddpwdc  12704  phicl2  12744  phibndlem  12746  phibnd  12747  hashdvds  12751  crth  12754  phimullem  12755  eulerthlemfi  12758  eulerthlemrprm  12759  eulerthlema  12760  hashgcdeq  12770  phisum  12771  oddprm  12790  prm23ge5  12795  pythagtriplem1  12796  pythagtriplem4  12799  pythagtriplem12  12806  pythagtriplem14  12808  pczpre  12828  pcadd  12871  pcmpt  12874  pockthlem  12887  pockthi  12889  infpnlem2  12891  gzreim  12910  4sqlem11  12932  4sqlem12  12933  4sqlem13m  12934  4sqlem17  12938  2expltfac  12970  evenennn  12972  ennnfonelemjn  12981  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ennnfonelemex  12993  ennnfonelemhom  12994  ennnfonelemnn0  13001  exmidunben  13005  ctinfomlemom  13006  ssnnctlemct  13025  nninfdc  13032  slotex  13067  setscom  13080  strslfv3  13086  setsslid  13091  bassetsnn  13097  basmex  13100  basmexd  13101  relelbasov  13103  ressbas2d  13109  ressbasid  13111  strressid  13112  ressval3d  13113  2strbas1g  13164  2strop1g  13165  rngbaseg  13177  rngplusgg  13178  rngmulrg  13179  srngbased  13188  srngplusgd  13189  srngmulrd  13190  srnginvld  13191  lmodbased  13206  lmodplusgd  13207  lmodscad  13208  lmodvscad  13209  ipsbased  13218  ipsaddgd  13219  ipsmulrd  13220  ipsscad  13221  ipsvscad  13222  ipsipd  13223  topgrpbasd  13238  topgrpplusgd  13239  topgrptsetd  13240  tgvalex  13304  prdsex  13310  prdsval  13314  prdsbaslemss  13315  prdsbas  13317  prdsplusg  13318  prdsmulr  13319  pwsbas  13333  pwselbasb  13334  pwssnf1o  13339  imasex  13346  imasival  13347  imasbas  13348  imasplusg  13349  imasmulr  13350  imasaddfn  13358  imasaddval  13359  imasaddf  13360  imasmulfn  13361  imasmulval  13362  imasmulf  13363  qusval  13364  qusex  13366  qusaddvallemg  13374  qusaddflemg  13375  qusaddval  13376  qusaddf  13377  qusmulval  13378  qusmulf  13379  xpsfval  13389  xpsval  13393  plusffvalg  13403  grpidvalg  13414  igsumvalx  13430  gsumfzval  13432  gsumress  13436  gsum0g  13437  gsumval2  13438  issubmnd  13483  ress0g  13484  ismhm  13502  mhmex  13503  issubm  13513  0mhm  13527  grppropstrg  13560  grpinvfvalg  13583  grpinvval  13584  grpinvfng  13585  grpsubfvalg  13586  grpsubval  13587  grpressid  13602  grplactfval  13642  qusgrp2  13658  mulgfvalg  13666  mulgex  13668  mulgnngsum  13672  issubg  13718  subgex  13721  subgmulg  13733  issubg2m  13734  releqgg  13765  eqgex  13766  eqgfval  13767  eqgen  13772  isghm  13788  ablressid  13880  mgptopng  13900  rngressid  13925  qusrng  13929  dfur2g  13933  ringidss  14000  ring1  14030  ringressid  14034  qusring2  14037  dvdsrvald  14065  dvdsrex  14070  unitgrp  14088  unitabl  14089  invrfvald  14094  unitlinv  14098  unitrinv  14099  dvrfvald  14105  rdivmuldivd  14116  invrpropdg  14121  rhmunitinv  14150  isnzr2  14156  issubrng  14171  issubrg  14193  subrgugrp  14212  subrgpropd  14225  rrgmex  14233  aprval  14254  islmod  14263  scaffvalg  14278  lssex  14326  lssmex  14327  lsssetm  14328  islssmg  14330  islss3  14351  lspfval  14360  lspval  14362  lspcl  14363  lspex  14367  sralemg  14410  srascag  14414  sravscag  14415  sraipg  14416  sraex  14418  rlmsubg  14430  rlmvnegg  14437  ixpsnbasval  14438  lidlvalg  14443  rspvalg  14444  lidlex  14445  rspex  14446  lidlmex  14447  lidlss  14448  lidlrsppropdg  14467  2idlmex  14473  qusrhm  14500  znlidl  14606  zncrng2  14607  znval  14608  znle  14609  znbaslemnn  14611  znbas  14616  znzrh2  14618  znzrhval  14619  znzrhfo  14620  zndvds  14621  znfi  14627  znhash  14628  znidom  14629  znidomb  14630  psrval  14638  psrbasg  14646  psrelbas  14647  psrplusgg  14650  psraddcl  14652  psr0cl  14653  psrnegcl  14655  psr1clfi  14660  mplvalcoe  14662  mplplusgg  14675  toponsspwpwg  14704  topgele  14711  istps  14714  topontopn  14719  tgclb  14747  lmfval  14875  lmres  14930  ispsmet  15005  psmetge0  15013  ismet  15026  isxmet  15027  xmetge0  15047  isxms2  15134  comet  15181  bdxmet  15183  cnmetdval  15211  cnbl0  15216  cnblcld  15217  reopnap  15228  tgioo  15236  cncfcncntop  15275  cncfmpt2fcntop  15281  maxcncf  15297  mincncf  15298  hovergt0  15332  limcimolemlt  15346  cnplimcim  15349  cnplimclemr  15351  limccnpcntop  15357  limccnp2lem  15358  limccnp2cntop  15359  dvfvalap  15363  dvbss  15367  dvcnp2cntop  15381  dvcn  15382  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvcjbr  15390  dvrecap  15395  dvmptfsum  15407  dveflem  15408  plyval  15414  plycolemc  15440  dvply2  15449  reeff1olem  15453  pilem3  15465  ef2kpi  15488  efper  15489  sinperlem  15490  efimpi  15501  ptolemy  15506  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  sinq12gt0  15512  cosq14gt0  15514  tangtx  15520  sinkpi  15529  coskpi  15530  cosordlem  15531  rplogcl  15561  logge0  15562  logdivlti  15563  logbleb  15643  logblt  15644  binom4  15661  wilthlem1  15662  1sgmprm  15676  1sgm2ppw  15677  mersenne  15679  perfect1  15680  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgsval2lem  15697  lgsval4a  15709  lgsneg  15711  lgsdilem  15714  lgsdirprm  15721  lgsdirnn0  15734  gausslemma2dlem0i  15744  gausslemma2dlem6  15754  gausslemma2dlem7  15755  gausslemma2d  15756  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgseisenlem4  15760  lgsquadlemofi  15763  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2lem2  15769  lgsquad2  15770  m1lgs  15772  2lgs  15791  2lgsoddprmlem2  15793  2lgsoddprm  15800  2sqlem2  15802  vtxvalg  15825  vtxex  15827  struct2slots2dom  15847  structvtxval  15848  structiedg0val  15849  structgrssvtx  15851  structgrssiedg  15852  edgstruct  15872  wlkv0  16090  upgr2wlkdc  16096  pwf1oexmid  16394  nnnninfex  16418  isomninnlem  16428  iswomninnlem  16447  ismkvnnlem  16450