Theorem sylancr 418

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 415	1 ⊢ (𝜑 → 𝜃)

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  4222  unipw  4359  opeluu  4598  uniexb  4621  unon  4660  onintrab2im  4667  xpexg  4891  resiexg  5111  imaexg  5143  exse2  5164  soirri  5185  djudisj  5218  elxp5  5279  cnvexg  5328  cnviinm  5332  coexg  5335  funssres  5423  f1oabexg  5654  sefvex  5719  ssimaex  5767  mptfvex  5794  f1ompt  5862  fmptcof  5878  resfunexg  5939  mptexg  5945  funfvima3  5955  ovid  6208  ov  6211  ofres  6321  cofunexg  6342  opabex3d  6354  opabex3  6355  oprabexd  6364  1stcof  6401  2ndcof  6402  mpoexxg  6450  cnvf1o  6465  f2ndf  6466  algrflemg  6470  tposexg  6533  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemi14d  6608  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemres  6624  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemres  6637  rdgtfr  6649  rdgruledefgg  6650  rdgon  6661  frecabex  6673  freccllem  6677  frecfcllem  6679  omcl  6738  oeicl  6739  erth  6857  th3qlem1  6915  mapex  6932  pmvalg  6937  mapfoss  6951  mapsnconst  6980  ixpexgg  7008  fundmen  7098  cnvct  7101  mapsnend  7103  snfig  7107  unen  7109  xpdom2  7133  mapxpen  7152  phplem2  7158  findcard2  7197  findcard2s  7198  infnfi  7203  relcnvfi  7259  sbthlemi8  7286  sbthlemi10  7288  fival  7309  fiss  7316  inl11  7411  casef  7434  caseinj  7435  caseinl  7437  caseinr  7438  djudom  7439  difinfsn  7446  djuinj  7452  0ct  7453  ctmlemr  7454  ctssdccl  7457  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  djuassen  7579  xpdjuen  7580  djudoml  7581  djudomr  7582  cc2lem  7638  ltnnnq  7796  nnnq0lem1  7819  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemfl  7948  mulnqprlemfu  7949  suplocexprlem2b  8087  prsrlem1  8115  gt0srpr  8121  caucvgsrlemcl  8162  caucvgsrlemfv  8164  caucvgsrlembound  8167  mulcnsr  8208  mulcnsrec  8216  addvalex  8217  pitoregt0  8222  axmulass  8246  axdistr  8247  recriota  8263  mulrid  8329  axmulgt0  8403  cnegexlem2  8509  cnegex  8511  gt0ne0d  8847  recexre  8914  msqge0  8952  mulge0  8955  aptap  8986  recgt0  9188  recreclt  9238  cju  9299  nnge1  9336  nnnlt1  9339  nn0nlt0  9600  nnnle0  9704  elz2  9727  nnm1ge0  9743  recnz  9750  zneo  9758  uz3m2nn  9989  eluz2b2  10019  nn01to3  10033  mnflt  10202  xnn0dcle  10221  xltadd1  10295  lincmb01cmp  10422  iccf1o  10424  fz1n  10465  fseq1p1m1  10518  fznn0  10537  fzctr  10557  4fvwrd4  10564  fzo0n  10592  elfzonlteqm1  10645  divfl0  10752  modqelico  10792  zmodfz  10804  modqid  10807  modqmuladdim  10825  m1modge3gt1  10829  addmodid  10830  frec2uzf1od  10864  frecfzennn  10884  frecfzen2  10885  fzfig  10888  ser0  10991  ser3le  10995  expgt1  11035  expubnd  11054  iexpcyc  11102  binom2sub  11111  binom3  11115  zesq  11117  bernneq  11119  bernneq2  11120  expnbnd  11122  expnlbnd2  11124  facdiv  11198  faclbnd2  11202  faclbnd3  11203  bcval4  11212  hashinfom  11239  hashennn  11241  fihashf1rn  11249  isfinite4im  11253  hashfz  11284  ssenneg  11302  hashf1lem1  11307  hashf1lem2  11308  iswrd  11328  iswrdiz  11333  wrdexg  11337  wrdexb  11338  wrdfin  11345  wrdnval  11357  wrdred1hash  11370  ccatsymb  11392  ccatalpha  11403  s111  11421  fzowrddc  11441  swrdlen  11446  swrdwrdsymbg  11458  pfxval  11468  pfx0g  11470  fnpfx  11471  pfxlen  11479  cats1un  11515  swrdccat  11529  crre  11644  crim  11645  remim  11647  mulreap  11651  cjreb  11653  recj  11654  reneg  11655  readd  11656  remullem  11658  imcj  11662  imneg  11663  imadd  11664  cjadd  11671  cjneg  11677  imval2  11681  cjreim  11691  cnrecnv  11698  uzin2  11775  absval  11789  rennim  11790  resqrexlemcalc3  11804  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemgt0  11808  resqrexlemga  11811  absreimsq  11855  absreim  11856  amgm2  11907  climconst2  12082  climshft  12095  climshft2  12097  reccn2ap  12104  climge0  12116  sumsnf  12201  sumnul  12216  isumcl  12217  fsum2dlemstep  12226  fisumcom2  12230  fsumabs  12257  fsumiun  12269  binom  12276  bcxmas  12281  arisum  12290  expcnvap0  12294  explecnv  12297  geosergap  12298  geolim  12303  geolim2  12304  geo2sum  12306  geo2lim  12308  cvgratnnlemrate  12322  cvgratz  12324  mertenslemi1  12327  prodf1  12334  prodeq2w  12348  fprodntrivap  12376  prodsnf  12384  fprod2dlemstep  12414  fprodcom2fi  12418  efcllemp  12450  ege2le3  12463  eftlub  12482  efgt1  12489  tanval2ap  12505  tanval3ap  12506  resinval  12507  recosval  12508  efi4p  12509  resin4p  12510  recos4p  12511  resincl  12512  recoscl  12513  efmival  12525  efeul  12526  sinadd  12528  cosadd  12529  tanaddap  12531  sinmul  12536  cos2tsin  12543  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  sin01gt0  12554  cos01gt0  12555  absef  12562  absefib  12563  efieq1re  12564  demoivreALT  12566  eirraplem  12569  3dvds  12656  odd2np1  12665  oddm1even  12667  oddp1even  12668  oexpneg  12669  opoe  12687  omoe  12688  nn0o1gt2  12697  nn0o  12699  bitsdc  12739  bitsfzolem  12746  bitsfzo  12747  bitsinv1lem  12753  bitsinv1  12754  nninfctlemfo  12842  algcvg  12851  algcvgblem  12852  1nprm  12917  1idssfct  12918  oddprmge3  12939  divgcdodd  12947  phicl2  13021  phibndlem  13023  phibnd  13024  hashdvds  13028  crth  13031  phimullem  13032  eulerthlemfi  13035  eulerthlemrprm  13036  eulerthlema  13037  hashgcdeq  13047  phisum  13048  oddprm  13067  prm23ge5  13072  pythagtriplem1  13073  pythagtriplem4  13076  pythagtriplem12  13083  pythagtriplem14  13085  pczpre  13105  pcadd  13148  pcmpt  13151  pockthlem  13164  pockthi  13166  infpnlem2  13168  gzreim  13187  4sqlem11  13209  4sqlem12  13210  4sqlem13m  13211  4sqlem17  13215  2expltfac  13248  prmlem0  13249  prmlem1  13251  prmlem2  13263  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemefi  13295  ballotfilemodife  13298  ballotfilem4  13299  evenennn  13342  ennnfonelemjn  13351  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemnn0  13371  exmidunben  13375  ctinfomlemom  13376  ssnnctlemct  13395  nninfdc  13402  slotex  13437  setscom  13450  strslfv3  13456  setsslid  13461  bassetsnn  13467  basmex  13470  basmexd  13471  relelbasov  13474  ressbas2d  13481  ressbasid  13483  strressid  13484  ressval3d  13485  2strbas1g  13536  2strop1g  13537  rngbaseg  13549  rngplusgg  13550  rngmulrg  13551  srngbased  13560  srngplusgd  13561  srngmulrd  13562  srnginvld  13563  lmodbased  13578  lmodplusgd  13579  lmodscad  13580  lmodvscad  13581  ipsbased  13590  ipsaddgd  13591  ipsmulrd  13592  ipsscad  13593  ipsvscad  13594  ipsipd  13595  topgrpbasd  13610  topgrpplusgd  13611  topgrptsetd  13612  tgvalex  13676  imasex  13685  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfn  13697  imasaddval  13698  imasaddf  13699  imasmulfn  13700  imasmulval  13701  imasmulf  13702  qusval  13703  qusex  13705  qusaddvallemg  13713  qusaddflemg  13714  qusaddval  13715  qusaddf  13716  qusmulval  13717  qusmulf  13718  xpsfval  13728  plusffvalg  13741  grpidvalg  13752  gzsumvalx  13768  gzsumfzval  13770  gzsumress  13771  gzsum0  13772  gzsumval2  13773  issubmnd  13814  ress0g  13815  ismhm  13827  mhmex  13828  issubm  13838  0mhm  13852  grppropstrg  13883  grpinvfvalg  13906  grpinvval  13907  grpinvfng  13908  grpsubfvalg  13909  grpsubval  13910  grpressid  13925  grplactfval  13965  qusgrp2  13975  mulgfvalg  13983  mulgex  13985  mulgnngzsum  13989  issubg  14035  subgex  14038  subgmulg  14050  issubg2m  14051  releqgg  14082  eqgex  14083  eqgfval  14084  eqgen  14089  isghm  14105  cntzex  14150  cntzfval  14152  cntzval  14153  cntz2ss  14168  ablressid  14229  gsumsncmn  14246  gsump1  14247  gsummptfidmadd  14251  gsummptfidmsplit  14254  prdsex  14279  prdsval  14280  prdsbaslemss  14281  prdsbas  14283  prdsplusg  14284  prdsmulr  14285  xpsval  14308  pwsbas  14312  pwselbasb  14313  pwssnf1o  14318  mgptopng  14335  rngressid  14360  qusrng  14364  dfur2g  14373  ringidss  14441  ring1  14471  ringressid  14477  qusring2  14480  opprringb  14495  dvdsrvald  14509  dvdsrex  14514  unitgrp  14532  unitabl  14533  invrfvald  14538  unitlinv  14542  unitrinv  14543  dvrfvald  14549  rdivmuldivd  14560  invrpropdg  14565  rhmunitinv  14594  isnzr2  14600  issubrng  14616  issubrg  14638  subrgugrp  14657  subrgpropd  14670  rrgmex  14678  aprval  14700  aprprop  14710  islmod  14736  scaffvalg  14752  lssex  14800  lssmex  14801  lsssetm  14802  islssmg  14804  islss3  14825  lspfval  14834  lspval  14836  lspcl  14837  lspex  14841  sralemg  14884  srascag  14888  sravscag  14889  sraipg  14890  sraex  14892  rlmsubg  14904  rlmvnegg  14911  ixpsnbasval  14912  lidlvalg  14917  rspvalg  14918  lidlex  14919  rspex  14920  lidlmex  14921  lidlss  14922  lidlrsppropdg  14941  2idlmex  14947  qusrhm  14974  gsumfsum  15032  znlidl  15078  zncrng2  15079  znval  15080  znle  15081  znbaslemnn  15083  znbas  15088  znzrh2  15090  znzrhval  15091  znzrhfo  15092  zndvds  15093  znfi  15099  znhash  15100  znidom  15101  znidomb  15102  aspval  15124  aspsubrg  15127  asclfval  15130  psrval  15159  psrbasg  15178  psrelbas  15179  psrplusgg  15182  psraddcl  15184  psrmulrg  15186  psrmulclfilem  15189  psr0cl  15191  psrnegcl  15193  psr1clfi  15198  psrlidmfi  15199  mplvalcoe  15206  mplplusgg  15219  toponsspwpwg  15248  topgele  15255  istps  15258  topontopn  15263  tgclb  15291  lmfval  15419  lmres  15474  ispsmet  15549  psmetge0  15557  ismet  15570  isxmet  15571  xmetge0  15591  isxms2  15678  comet  15725  bdxmet  15727  cnmetdval  15755  cnbl0  15760  cnblcld  15761  reopnap  15772  tgioo  15780  cncfcncntop  15819  cncfmpt2fcntop  15825  maxcncf  15841  mincncf  15842  hovergt0  15876  limcimolemlt  15890  cnplimcim  15893  cnplimclemr  15895  limccnpcntop  15901  limccnp2lem  15902  limccnp2cntop  15903  dvfvalap  15907  dvbss  15911  dvcnp2cntop  15925  dvcn  15926  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvrecap  15939  dvmptfsum  15951  dveflem  15952  plyval  15958  plycolemc  15984  dvply2  15993  reeff1olem  15997  pilem3  16010  ef2kpi  16033  efper  16034  sinperlem  16035  efimpi  16046  ptolemy  16051  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  cosq14gt0  16059  tangtx  16065  sinkpi  16074  coskpi  16075  cosordlem  16077  rplogcl  16109  logge0  16110  logdivlti  16111  logbleb  16197  logblt  16198  binom4  16219  log2tlbndlog2  16220  log2ublem2  16222  log2ublog2  16224  birthdaylem2  16226  wilthlem1  16232  ppiqsval  16240  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  ppiqeq0  16280  1sgmprm  16288  1sgm2ppw  16289  ppiublem1  16291  ppiqub  16293  chtqleppi  16294  chtublem  16295  chtqub  16296  mersenne  16297  perfect1  16298  perfectlem1  16299  perfectlem2  16300  perfect  16301  bcmono  16304  bcmax  16305  bclbnd  16307  bpos1lem  16309  bpos1  16310  bposlem1  16311  bposlem2  16312  bposlem3  16313  bposlem4  16314  bposlem5  16315  bposlem6  16316  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgsval2lem  16334  lgsval4a  16346  lgsneg  16348  lgsdilem  16351  lgsdirprm  16358  lgsdirnn0  16371  gausslemma2dlem0i  16381  gausslemma2dlem6  16391  gausslemma2dlem7  16392  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgsquadlemofi  16400  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem2  16406  lgsquad2  16407  m1lgs  16409  2lgs  16428  2lgsoddprmlem2  16430  2lgsoddprm  16437  2sqlem2  16439  vtxvalg  16462  vtxex  16464  struct2slots2dom  16484  structvtxval  16485  structiedg0val  16486  structgrssvtx  16488  structgrssiedg  16489  edgstruct  16510  vdegp1bid  16761  wlkv0  16815  upgr2wlkdc  16823  clwwlkex  16844  clwwlkccatlem  16846  eupthfi  16897  trlsegvdeglem6  16911  konigsberglem1  16934  konigsberglem5  16938  depindlem1  16952  pwf1oexmid  17234  nnnninfex  17271  repiecege0  17282  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309