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  5875  mptexg  5879  funfvima3  5888  ovid  6138  ov  6141  ofres  6250  cofunexg  6271  opabex3d  6283  opabex3  6284  oprabexd  6289  1stcof  6326  2ndcof  6327  mpoexxg  6375  cnvf1o  6390  f2ndf  6391  algrflemg  6395  tposexg  6424  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemi14d  6499  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemres  6528  rdgtfr  6540  rdgruledefgg  6541  rdgon  6552  frecabex  6564  freccllem  6568  frecfcllem  6570  omcl  6629  oeicl  6630  erth  6748  th3qlem1  6806  mapex  6823  pmvalg  6828  mapsnconst  6863  ixpexgg  6891  fundmen  6981  cnvct  6984  snfig  6989  unen  6991  xpdom2  7015  mapxpen  7034  phplem2  7039  findcard2  7078  findcard2s  7079  infnfi  7084  relcnvfi  7140  sbthlemi8  7163  sbthlemi10  7165  fival  7169  fiss  7176  inl11  7264  casef  7287  caseinj  7288  caseinl  7290  caseinr  7291  djudom  7292  difinfsn  7299  djuinj  7305  0ct  7306  ctmlemr  7307  ctssdccl  7310  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  djuassen  7432  xpdjuen  7433  djudoml  7434  djudomr  7435  cc2lem  7485  ltnnnq  7643  nnnq0lem1  7666  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemfl  7795  mulnqprlemfu  7796  suplocexprlem2b  7934  prsrlem1  7962  gt0srpr  7968  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsrlembound  8014  mulcnsr  8055  mulcnsrec  8063  addvalex  8064  pitoregt0  8069  axmulass  8093  axdistr  8094  recriota  8110  mulrid  8176  axmulgt0  8251  cnegexlem2  8355  cnegex  8357  gt0ne0d  8692  recexre  8758  msqge0  8796  mulge0  8799  aptap  8830  recgt0  9030  recreclt  9080  cju  9141  nnge1  9166  nnnlt1  9169  nn0nlt0  9428  nnnle0  9528  elz2  9551  nnm1ge0  9566  recnz  9573  zneo  9581  uz3m2nn  9807  eluz2b2  9837  nn01to3  9851  mnflt  10018  xnn0dcle  10037  xltadd1  10111  lincmb01cmp  10238  iccf1o  10239  fz1n  10279  fseq1p1m1  10329  fznn0  10348  fzctr  10368  4fvwrd4  10375  fzo0n  10403  elfzonlteqm1  10456  divfl0  10557  modqelico  10597  zmodfz  10609  modqid  10612  modqmuladdim  10630  m1modge3gt1  10634  addmodid  10635  frec2uzf1od  10669  frecfzennn  10689  frecfzen2  10690  fzfig  10693  ser0  10796  ser3le  10800  expgt1  10840  expubnd  10859  iexpcyc  10907  binom2sub  10916  binom3  10920  zesq  10921  bernneq  10923  bernneq2  10924  expnbnd  10926  expnlbnd2  10928  facdiv  11001  faclbnd2  11005  faclbnd3  11006  bcval4  11015  hashinfom  11041  hashennn  11043  fihashf1rn  11051  isfinite4im  11055  hashfz  11086  iswrd  11119  iswrdiz  11124  wrdexg  11128  wrdexb  11129  wrdfin  11136  wrdnval  11148  wrdred1hash  11161  ccatsymb  11183  ccatalpha  11194  s111  11212  fzowrddc  11232  swrdlen  11237  swrdwrdsymbg  11249  pfxval  11259  pfx0g  11261  fnpfx  11262  pfxlen  11270  cats1un  11306  swrdccat  11320  crre  11435  crim  11436  remim  11438  mulreap  11442  cjreb  11444  recj  11445  reneg  11446  readd  11447  remullem  11449  imcj  11453  imneg  11454  imadd  11455  cjadd  11462  cjneg  11468  imval2  11472  cjreim  11481  cnrecnv  11488  uzin2  11565  absval  11579  rennim  11580  resqrexlemcalc3  11594  resqrexlemnm  11596  resqrexlemcvg  11597  resqrexlemgt0  11598  resqrexlemga  11601  absreimsq  11645  absreim  11646  amgm2  11696  climconst2  11869  climshft  11882  climshft2  11884  reccn2ap  11891  climge0  11903  sumsnf  11988  sumnul  12003  isumcl  12004  fsum2dlemstep  12013  fisumcom2  12017  fsumabs  12044  fsumiun  12056  binom  12063  bcxmas  12068  arisum  12077  expcnvap0  12081  explecnv  12084  geosergap  12085  geolim  12090  geolim2  12091  geo2sum  12093  geo2lim  12095  cvgratnnlemrate  12109  cvgratz  12111  mertenslemi1  12114  prodf1  12121  prodeq2w  12135  fprodntrivap  12163  prodsnf  12171  fprod2dlemstep  12201  fprodcom2fi  12205  efcllemp  12237  ege2le3  12250  eftlub  12269  efgt1  12276  tanval2ap  12292  tanval3ap  12293  resinval  12294  recosval  12295  efi4p  12296  resin4p  12297  recos4p  12298  resincl  12299  recoscl  12300  efmival  12312  efeul  12313  sinadd  12315  cosadd  12316  tanaddap  12318  sinmul  12323  cos2tsin  12330  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  sin01gt0  12341  cos01gt0  12342  absef  12349  absefib  12350  efieq1re  12351  demoivreALT  12353  eirraplem  12356  3dvds  12443  odd2np1  12452  oddm1even  12454  oddp1even  12455  oexpneg  12456  opoe  12474  omoe  12475  nn0o1gt2  12484  nn0o  12486  bitsdc  12526  bitsfzolem  12533  bitsfzo  12534  bitsinv1lem  12540  bitsinv1  12541  nninfctlemfo  12629  algcvg  12638  algcvgblem  12639  1nprm  12704  1idssfct  12705  oddprmge3  12725  divgcdodd  12733  pw2dvdslemn  12755  pw2dvds  12756  oddpwdclemodd  12762  oddpwdc  12764  phicl2  12804  phibndlem  12806  phibnd  12807  hashdvds  12811  crth  12814  phimullem  12815  eulerthlemfi  12818  eulerthlemrprm  12819  eulerthlema  12820  hashgcdeq  12830  phisum  12831  oddprm  12850  prm23ge5  12855  pythagtriplem1  12856  pythagtriplem4  12859  pythagtriplem12  12866  pythagtriplem14  12868  pczpre  12888  pcadd  12931  pcmpt  12934  pockthlem  12947  pockthi  12949  infpnlem2  12951  gzreim  12970  4sqlem11  12992  4sqlem12  12993  4sqlem13m  12994  4sqlem17  12998  2expltfac  13030  evenennn  13032  ennnfonelemjn  13041  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemnn0  13061  exmidunben  13065  ctinfomlemom  13066  ssnnctlemct  13085  nninfdc  13092  slotex  13127  setscom  13140  strslfv3  13146  setsslid  13151  bassetsnn  13157  basmex  13160  basmexd  13161  relelbasov  13163  ressbas2d  13169  ressbasid  13171  strressid  13172  ressval3d  13173  2strbas1g  13224  2strop1g  13225  rngbaseg  13237  rngplusgg  13238  rngmulrg  13239  srngbased  13248  srngplusgd  13249  srngmulrd  13250  srnginvld  13251  lmodbased  13266  lmodplusgd  13267  lmodscad  13268  lmodvscad  13269  ipsbased  13278  ipsaddgd  13279  ipsmulrd  13280  ipsscad  13281  ipsvscad  13282  ipsipd  13283  topgrpbasd  13298  topgrpplusgd  13299  topgrptsetd  13300  tgvalex  13364  prdsex  13370  prdsval  13374  prdsbaslemss  13375  prdsbas  13377  prdsplusg  13378  prdsmulr  13379  pwsbas  13393  pwselbasb  13394  pwssnf1o  13399  imasex  13406  imasival  13407  imasbas  13408  imasplusg  13409  imasmulr  13410  imasaddfn  13418  imasaddval  13419  imasaddf  13420  imasmulfn  13421  imasmulval  13422  imasmulf  13423  qusval  13424  qusex  13426  qusaddvallemg  13434  qusaddflemg  13435  qusaddval  13436  qusaddf  13437  qusmulval  13438  qusmulf  13439  xpsfval  13449  xpsval  13453  plusffvalg  13463  grpidvalg  13474  igsumvalx  13490  gsumfzval  13492  gsumress  13496  gsum0g  13497  gsumval2  13498  issubmnd  13543  ress0g  13544  ismhm  13562  mhmex  13563  issubm  13573  0mhm  13587  grppropstrg  13620  grpinvfvalg  13643  grpinvval  13644  grpinvfng  13645  grpsubfvalg  13646  grpsubval  13647  grpressid  13662  grplactfval  13702  qusgrp2  13718  mulgfvalg  13726  mulgex  13728  mulgnngsum  13732  issubg  13778  subgex  13781  subgmulg  13793  issubg2m  13794  releqgg  13825  eqgex  13826  eqgfval  13827  eqgen  13832  isghm  13848  ablressid  13940  mgptopng  13961  rngressid  13986  qusrng  13990  dfur2g  13994  ringidss  14061  ring1  14091  ringressid  14095  qusring2  14098  dvdsrvald  14126  dvdsrex  14131  unitgrp  14149  unitabl  14150  invrfvald  14155  unitlinv  14159  unitrinv  14160  dvrfvald  14166  rdivmuldivd  14177  invrpropdg  14182  rhmunitinv  14211  isnzr2  14217  issubrng  14232  issubrg  14254  subrgugrp  14273  subrgpropd  14286  rrgmex  14294  aprval  14315  islmod  14324  scaffvalg  14339  lssex  14387  lssmex  14388  lsssetm  14389  islssmg  14391  islss3  14412  lspfval  14421  lspval  14423  lspcl  14424  lspex  14428  sralemg  14471  srascag  14475  sravscag  14476  sraipg  14477  sraex  14479  rlmsubg  14491  rlmvnegg  14498  ixpsnbasval  14499  lidlvalg  14504  rspvalg  14505  lidlex  14506  rspex  14507  lidlmex  14508  lidlss  14509  lidlrsppropdg  14528  2idlmex  14534  qusrhm  14561  znlidl  14667  zncrng2  14668  znval  14669  znle  14670  znbaslemnn  14672  znbas  14677  znzrh2  14679  znzrhval  14680  znzrhfo  14681  zndvds  14682  znfi  14688  znhash  14689  znidom  14690  znidomb  14691  psrval  14699  psrbasg  14707  psrelbas  14708  psrplusgg  14711  psraddcl  14713  psr0cl  14714  psrnegcl  14716  psr1clfi  14721  mplvalcoe  14723  mplplusgg  14736  toponsspwpwg  14765  topgele  14772  istps  14775  topontopn  14780  tgclb  14808  lmfval  14936  lmres  14991  ispsmet  15066  psmetge0  15074  ismet  15087  isxmet  15088  xmetge0  15108  isxms2  15195  comet  15242  bdxmet  15244  cnmetdval  15272  cnbl0  15277  cnblcld  15278  reopnap  15289  tgioo  15297  cncfcncntop  15336  cncfmpt2fcntop  15342  maxcncf  15358  mincncf  15359  hovergt0  15393  limcimolemlt  15407  cnplimcim  15410  cnplimclemr  15412  limccnpcntop  15418  limccnp2lem  15419  limccnp2cntop  15420  dvfvalap  15424  dvbss  15428  dvcnp2cntop  15442  dvcn  15443  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvrecap  15456  dvmptfsum  15468  dveflem  15469  plyval  15475  plycolemc  15501  dvply2  15510  reeff1olem  15514  pilem3  15526  ef2kpi  15549  efper  15550  sinperlem  15551  efimpi  15562  ptolemy  15567  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  cosq14gt0  15575  tangtx  15581  sinkpi  15590  coskpi  15591  cosordlem  15592  rplogcl  15622  logge0  15623  logdivlti  15624  logbleb  15704  logblt  15705  binom4  15722  wilthlem1  15723  1sgmprm  15737  1sgm2ppw  15738  mersenne  15740  perfect1  15741  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgsval2lem  15758  lgsval4a  15770  lgsneg  15772  lgsdilem  15775  lgsdirprm  15782  lgsdirnn0  15795  gausslemma2dlem0i  15805  gausslemma2dlem6  15815  gausslemma2dlem7  15816  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlemofi  15824  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem2  15830  lgsquad2  15831  m1lgs  15833  2lgs  15852  2lgsoddprmlem2  15854  2lgsoddprm  15861  2sqlem2  15863  vtxvalg  15886  vtxex  15888  struct2slots2dom  15908  structvtxval  15909  structiedg0val  15910  structgrssvtx  15912  structgrssiedg  15913  edgstruct  15934  vdegp1bid  16185  wlkv0  16239  upgr2wlkdc  16247  clwwlkex  16268  clwwlkccatlem  16270  eupthfi  16321  trlsegvdeglem6  16335  konigsberglem1  16358  konigsberglem5  16362  depindlem1  16376  pwf1oexmid  16651  nnnninfex  16675  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708  gfsumsn  16737  gfsump1  16738