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  4172  unipw  4302  opeluu  4538  uniexb  4561  unon  4600  onintrab2im  4607  xpexg  4830  resiexg  5046  imaexg  5078  exse2  5098  soirri  5119  djudisj  5152  elxp5  5213  cnvexg  5262  cnviinm  5266  coexg  5269  funssres  5356  f1oabexg  5580  sefvex  5644  ssimaex  5688  mptfvex  5713  f1ompt  5779  fmptcof  5795  resfunexg  5853  mptexg  5857  funfvima3  5866  ovid  6112  ov  6115  ofres  6223  cofunexg  6244  opabex3d  6256  opabex3  6257  oprabexd  6262  1stcof  6299  2ndcof  6300  mpoexxg  6346  cnvf1o  6361  f2ndf  6362  algrflemg  6366  tposexg  6394  tfrlemisucaccv  6461  tfrlemibxssdm  6463  tfrlemibfn  6464  tfrlemi14d  6469  tfr1onlemsucaccv  6477  tfr1onlembxssdm  6479  tfr1onlembfn  6480  tfr1onlemres  6485  tfrcllemsucaccv  6490  tfrcllembxssdm  6492  tfrcllembfn  6493  tfrcllemres  6498  rdgtfr  6510  rdgruledefgg  6511  rdgon  6522  frecabex  6534  freccllem  6538  frecfcllem  6540  omcl  6597  oeicl  6598  erth  6716  th3qlem1  6774  mapex  6791  pmvalg  6796  mapsnconst  6831  ixpexgg  6859  fundmen  6949  cnvct  6952  snfig  6957  unen  6959  xpdom2  6978  mapxpen  6997  phplem2  7002  findcard2  7039  findcard2s  7040  infnfi  7045  relcnvfi  7096  sbthlemi8  7119  sbthlemi10  7121  fival  7125  fiss  7132  inl11  7220  casef  7243  caseinj  7244  caseinl  7246  caseinr  7247  djudom  7248  difinfsn  7255  djuinj  7261  0ct  7262  ctmlemr  7263  ctssdccl  7266  enomnilem  7293  enmkvlem  7316  enwomnilem  7324  djuassen  7387  xpdjuen  7388  djudoml  7389  djudomr  7390  cc2lem  7440  ltnnnq  7598  nnnq0lem1  7621  addnqprlemfl  7734  addnqprlemfu  7735  mulnqprlemfl  7750  mulnqprlemfu  7751  suplocexprlem2b  7889  prsrlem1  7917  gt0srpr  7923  caucvgsrlemcl  7964  caucvgsrlemfv  7966  caucvgsrlembound  7969  mulcnsr  8010  mulcnsrec  8018  addvalex  8019  pitoregt0  8024  axmulass  8048  axdistr  8049  recriota  8065  mulrid  8131  axmulgt0  8206  cnegexlem2  8310  cnegex  8312  gt0ne0d  8647  recexre  8713  msqge0  8751  mulge0  8754  aptap  8785  recgt0  8985  recreclt  9035  cju  9096  nnge1  9121  nnnlt1  9124  nn0nlt0  9383  nnnle0  9483  elz2  9506  nnm1ge0  9521  recnz  9528  zneo  9536  uz3m2nn  9756  eluz2b2  9786  nn01to3  9800  mnflt  9967  xnn0dcle  9986  xltadd1  10060  lincmb01cmp  10187  iccf1o  10188  fz1n  10228  fseq1p1m1  10278  fznn0  10297  fzctr  10317  4fvwrd4  10324  fzo0n  10352  elfzonlteqm1  10403  divfl0  10503  modqelico  10543  zmodfz  10555  modqid  10558  modqmuladdim  10576  m1modge3gt1  10580  addmodid  10581  frec2uzf1od  10615  frecfzennn  10635  frecfzen2  10636  fzfig  10639  ser0  10742  ser3le  10746  expgt1  10786  expubnd  10805  iexpcyc  10853  binom2sub  10862  binom3  10866  zesq  10867  bernneq  10869  bernneq2  10870  expnbnd  10872  expnlbnd2  10874  facdiv  10947  faclbnd2  10951  faclbnd3  10952  bcval4  10961  hashinfom  10987  hashennn  10989  fihashf1rn  10997  isfinite4im  11001  hashfz  11030  iswrd  11060  iswrdiz  11065  wrdexg  11069  wrdexb  11070  wrdfin  11077  wrdnval  11088  wrdred1hash  11101  ccatsymb  11123  s111  11150  fzowrddc  11165  swrdlen  11170  swrdwrdsymbg  11182  pfxval  11192  pfx0g  11194  fnpfx  11195  pfxlen  11203  cats1un  11239  swrdccat  11253  crre  11354  crim  11355  remim  11357  mulreap  11361  cjreb  11363  recj  11364  reneg  11365  readd  11366  remullem  11368  imcj  11372  imneg  11373  imadd  11374  cjadd  11381  cjneg  11387  imval2  11391  cjreim  11400  cnrecnv  11407  uzin2  11484  absval  11498  rennim  11499  resqrexlemcalc3  11513  resqrexlemnm  11515  resqrexlemcvg  11516  resqrexlemgt0  11517  resqrexlemga  11520  absreimsq  11564  absreim  11565  amgm2  11615  climconst2  11788  climshft  11801  climshft2  11803  reccn2ap  11810  climge0  11822  sumsnf  11906  sumnul  11921  isumcl  11922  fsum2dlemstep  11931  fisumcom2  11935  fsumabs  11962  fsumiun  11974  binom  11981  bcxmas  11986  arisum  11995  expcnvap0  11999  explecnv  12002  geosergap  12003  geolim  12008  geolim2  12009  geo2sum  12011  geo2lim  12013  cvgratnnlemrate  12027  cvgratz  12029  mertenslemi1  12032  prodf1  12039  prodeq2w  12053  fprodntrivap  12081  prodsnf  12089  fprod2dlemstep  12119  fprodcom2fi  12123  efcllemp  12155  ege2le3  12168  eftlub  12187  efgt1  12194  tanval2ap  12210  tanval3ap  12211  resinval  12212  recosval  12213  efi4p  12214  resin4p  12215  recos4p  12216  resincl  12217  recoscl  12218  efmival  12230  efeul  12231  sinadd  12233  cosadd  12234  tanaddap  12236  sinmul  12241  cos2tsin  12248  ef01bndlem  12253  sin01bnd  12254  cos01bnd  12255  sin01gt0  12259  cos01gt0  12260  absef  12267  absefib  12268  efieq1re  12269  demoivreALT  12271  eirraplem  12274  3dvds  12361  odd2np1  12370  oddm1even  12372  oddp1even  12373  oexpneg  12374  opoe  12392  omoe  12393  nn0o1gt2  12402  nn0o  12404  bitsdc  12444  bitsfzolem  12451  bitsfzo  12452  bitsinv1lem  12458  bitsinv1  12459  nninfctlemfo  12547  algcvg  12556  algcvgblem  12557  1nprm  12622  1idssfct  12623  oddprmge3  12643  divgcdodd  12651  pw2dvdslemn  12673  pw2dvds  12674  oddpwdclemodd  12680  oddpwdc  12682  phicl2  12722  phibndlem  12724  phibnd  12725  hashdvds  12729  crth  12732  phimullem  12733  eulerthlemfi  12736  eulerthlemrprm  12737  eulerthlema  12738  hashgcdeq  12748  phisum  12749  oddprm  12768  prm23ge5  12773  pythagtriplem1  12774  pythagtriplem4  12777  pythagtriplem12  12784  pythagtriplem14  12786  pczpre  12806  pcadd  12849  pcmpt  12852  pockthlem  12865  pockthi  12867  infpnlem2  12869  gzreim  12888  4sqlem11  12910  4sqlem12  12911  4sqlem13m  12912  4sqlem17  12916  2expltfac  12948  evenennn  12950  ennnfonelemjn  12959  ennnfonelemkh  12969  ennnfonelemhf1o  12970  ennnfonelemex  12971  ennnfonelemhom  12972  ennnfonelemnn0  12979  exmidunben  12983  ctinfomlemom  12984  ssnnctlemct  13003  nninfdc  13010  slotex  13045  setscom  13058  strslfv3  13064  setsslid  13069  bassetsnn  13075  basmex  13078  basmexd  13079  relelbasov  13081  ressbas2d  13087  ressbasid  13089  strressid  13090  ressval3d  13091  2strbas1g  13142  2strop1g  13143  rngbaseg  13155  rngplusgg  13156  rngmulrg  13157  srngbased  13166  srngplusgd  13167  srngmulrd  13168  srnginvld  13169  lmodbased  13184  lmodplusgd  13185  lmodscad  13186  lmodvscad  13187  ipsbased  13196  ipsaddgd  13197  ipsmulrd  13198  ipsscad  13199  ipsvscad  13200  ipsipd  13201  topgrpbasd  13216  topgrpplusgd  13217  topgrptsetd  13218  tgvalex  13282  prdsex  13288  prdsval  13292  prdsbaslemss  13293  prdsbas  13295  prdsplusg  13296  prdsmulr  13297  pwsbas  13311  pwselbasb  13312  pwssnf1o  13317  imasex  13324  imasival  13325  imasbas  13326  imasplusg  13327  imasmulr  13328  imasaddfn  13336  imasaddval  13337  imasaddf  13338  imasmulfn  13339  imasmulval  13340  imasmulf  13341  qusval  13342  qusex  13344  qusaddvallemg  13352  qusaddflemg  13353  qusaddval  13354  qusaddf  13355  qusmulval  13356  qusmulf  13357  xpsfval  13367  xpsval  13371  plusffvalg  13381  grpidvalg  13392  igsumvalx  13408  gsumfzval  13410  gsumress  13414  gsum0g  13415  gsumval2  13416  issubmnd  13461  ress0g  13462  ismhm  13480  mhmex  13481  issubm  13491  0mhm  13505  grppropstrg  13538  grpinvfvalg  13561  grpinvval  13562  grpinvfng  13563  grpsubfvalg  13564  grpsubval  13565  grpressid  13580  grplactfval  13620  qusgrp2  13636  mulgfvalg  13644  mulgex  13646  mulgnngsum  13650  issubg  13696  subgex  13699  subgmulg  13711  issubg2m  13712  releqgg  13743  eqgex  13744  eqgfval  13745  eqgen  13750  isghm  13766  ablressid  13858  mgptopng  13878  rngressid  13903  qusrng  13907  dfur2g  13911  ringidss  13978  ring1  14008  ringressid  14012  qusring2  14015  reldvdsrsrg  14041  dvdsrvald  14042  dvdsrex  14047  unitgrp  14065  unitabl  14066  invrfvald  14071  unitlinv  14075  unitrinv  14076  dvrfvald  14082  rdivmuldivd  14093  invrpropdg  14098  rhmunitinv  14127  isnzr2  14133  issubrng  14148  issubrg  14170  subrgugrp  14189  subrgpropd  14202  rrgmex  14210  aprval  14231  islmod  14240  scaffvalg  14255  lssex  14303  lssmex  14304  lsssetm  14305  islssmg  14307  islss3  14328  lspfval  14337  lspval  14339  lspcl  14340  lspex  14344  sralemg  14387  srascag  14391  sravscag  14392  sraipg  14393  sraex  14395  rlmsubg  14407  rlmvnegg  14414  ixpsnbasval  14415  lidlvalg  14420  rspvalg  14421  lidlex  14422  rspex  14423  lidlmex  14424  lidlss  14425  lidlrsppropdg  14444  2idlmex  14450  qusrhm  14477  znlidl  14583  zncrng2  14584  znval  14585  znle  14586  znbaslemnn  14588  znbas  14593  znzrh2  14595  znzrhval  14596  znzrhfo  14597  zndvds  14598  znfi  14604  znhash  14605  znidom  14606  znidomb  14607  psrval  14615  psrbasg  14623  psrelbas  14624  psrplusgg  14627  psraddcl  14629  psr0cl  14630  psrnegcl  14632  psr1clfi  14637  mplvalcoe  14639  mplplusgg  14652  toponsspwpwg  14681  topgele  14688  istps  14691  topontopn  14696  tgclb  14724  lmfval  14851  lmres  14907  ispsmet  14982  psmetge0  14990  ismet  15003  isxmet  15004  xmetge0  15024  isxms2  15111  comet  15158  bdxmet  15160  cnmetdval  15188  cnbl0  15193  cnblcld  15194  reopnap  15205  tgioo  15213  cncfcncntop  15252  cncfmpt2fcntop  15258  maxcncf  15274  mincncf  15275  hovergt0  15309  limcimolemlt  15323  cnplimcim  15326  cnplimclemr  15328  limccnpcntop  15334  limccnp2lem  15335  limccnp2cntop  15336  dvfvalap  15340  dvbss  15344  dvcnp2cntop  15358  dvcn  15359  dvaddxxbr  15360  dvmulxxbr  15361  dvcoapbr  15366  dvcjbr  15367  dvrecap  15372  dvmptfsum  15384  dveflem  15385  plyval  15391  plycolemc  15417  dvply2  15426  reeff1olem  15430  pilem3  15442  ef2kpi  15465  efper  15466  sinperlem  15467  efimpi  15478  ptolemy  15483  sincosq2sgn  15486  sincosq3sgn  15487  sincosq4sgn  15488  sinq12gt0  15489  cosq14gt0  15491  tangtx  15497  sinkpi  15506  coskpi  15507  cosordlem  15508  rplogcl  15538  logge0  15539  logdivlti  15540  logbleb  15620  logblt  15621  binom4  15638  wilthlem1  15639  1sgmprm  15653  1sgm2ppw  15654  mersenne  15656  perfect1  15657  perfectlem1  15658  perfectlem2  15659  perfect  15660  lgsval2lem  15674  lgsval4a  15686  lgsneg  15688  lgsdilem  15691  lgsdirprm  15698  lgsdirnn0  15711  gausslemma2dlem0i  15721  gausslemma2dlem6  15731  gausslemma2dlem7  15732  gausslemma2d  15733  lgseisenlem1  15734  lgseisenlem2  15735  lgseisenlem3  15736  lgseisenlem4  15737  lgsquadlemofi  15740  lgsquadlem1  15741  lgsquadlem2  15742  lgsquadlem3  15743  lgsquad2lem2  15746  lgsquad2  15747  m1lgs  15749  2lgs  15768  2lgsoddprmlem2  15770  2lgsoddprm  15777  2sqlem2  15779  vtxvalg  15802  vtxex  15804  struct2slots2dom  15824  structvtxval  15825  structiedg0val  15826  structgrssvtx  15828  structgrssiedg  15829  edgstruct  15849  pwf1oexmid  16296  nnnninfex  16319  isomninnlem  16329  iswomninnlem  16348  ismkvnnlem  16351