Theorem sylancr 411

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mpteq2da  4025  unipw  4147  opeluu  4379  uniexb  4402  unon  4435  onintrab2im  4442  xpexg  4661  resiexg  4872  imaexg  4901  exse2  4921  soirri  4941  djudisj  4974  elxp5  5035  cnvexg  5084  cnviinm  5088  coexg  5091  funssres  5173  f1oabexg  5387  sefvex  5450  ssimaex  5490  mptfvex  5514  f1ompt  5579  fmptcof  5595  resfunexg  5649  mptexg  5653  funfvima3  5659  ovid  5895  ov  5898  ofres  6004  cofunexg  6017  opabex3d  6027  opabex3  6028  oprabexd  6033  1stcof  6069  2ndcof  6070  mpoexxg  6116  cnvf1o  6130  f2ndf  6131  algrflemg  6135  tposexg  6163  tfrlemisucaccv  6230  tfrlemibxssdm  6232  tfrlemibfn  6233  tfrlemi14d  6238  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemres  6254  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemres  6267  rdgtfr  6279  rdgruledefgg  6280  rdgon  6291  frecabex  6303  freccllem  6307  frecfcllem  6309  omcl  6365  oeicl  6366  erth  6481  th3qlem1  6539  mapex  6556  pmvalg  6561  mapsnconst  6596  ixpexgg  6624  fundmen  6708  cnvct  6711  snfig  6716  unen  6718  xpdom2  6733  mapxpen  6750  phplem2  6755  findcard2  6791  findcard2s  6792  infnfi  6797  relcnvfi  6837  sbthlemi8  6860  sbthlemi10  6862  fival  6866  fiss  6873  inl11  6958  casef  6981  caseinj  6982  caseinl  6984  caseinr  6985  djudom  6986  difinfsn  6993  djuinj  6999  0ct  7000  ctmlemr  7001  ctssdccl  7004  enomnilem  7018  enmkvlem  7043  enwomnilem  7050  djuassen  7090  xpdjuen  7091  djudoml  7092  djudomr  7093  cc2lem  7098  ltnnnq  7255  nnnq0lem1  7278  addnqprlemfl  7391  addnqprlemfu  7392  mulnqprlemfl  7407  mulnqprlemfu  7408  suplocexprlem2b  7546  prsrlem1  7574  gt0srpr  7580  caucvgsrlemcl  7621  caucvgsrlemfv  7623  caucvgsrlembound  7626  mulcnsr  7667  mulcnsrec  7675  addvalex  7676  pitoregt0  7681  axmulass  7705  axdistr  7706  recriota  7722  mulid1  7787  axmulgt0  7860  cnegexlem2  7962  cnegex  7964  gt0ne0d  8298  recexre  8364  msqge0  8402  mulge0  8405  recgt0  8632  recreclt  8682  cju  8743  nnge1  8767  nnnlt1  8770  nn0nlt0  9027  elz2  9146  nnm1ge0  9161  recnz  9168  zneo  9176  uz3m2nn  9395  eluz2b2  9424  nn01to3  9436  mnflt  9599  xltadd1  9689  lincmb01cmp  9816  iccf1o  9817  fz1n  9855  fseq1p1m1  9905  fznn0  9924  fzctr  9941  4fvwrd4  9948  elfzonlteqm1  10018  divfl0  10100  modqelico  10138  zmodfz  10150  modqid  10153  modqmuladdim  10171  m1modge3gt1  10175  addmodid  10176  frec2uzf1od  10210  frecfzennn  10230  frecfzen2  10231  fzfig  10234  ser0  10318  ser3le  10322  expgt1  10362  expubnd  10381  iexpcyc  10428  binom2sub  10436  binom3  10440  zesq  10441  bernneq  10443  bernneq2  10444  expnbnd  10446  expnlbnd2  10448  facdiv  10516  faclbnd2  10520  faclbnd3  10521  bcval4  10530  hashinfom  10556  hashennn  10558  fihashf1rn  10567  isfinite4im  10571  hashfz  10599  crre  10661  crim  10662  remim  10664  mulreap  10668  cjreb  10670  recj  10671  reneg  10672  readd  10673  remullem  10675  imcj  10679  imneg  10680  imadd  10681  cjadd  10688  cjneg  10694  imval2  10698  cjreim  10707  cnrecnv  10714  uzin2  10791  absval  10805  rennim  10806  resqrexlemcalc3  10820  resqrexlemnm  10822  resqrexlemcvg  10823  resqrexlemgt0  10824  resqrexlemga  10827  absreimsq  10871  absreim  10872  amgm2  10922  climconst2  11092  climshft  11105  climshft2  11107  reccn2ap  11114  climge0  11126  sumsnf  11210  sumnul  11225  isumcl  11226  fsum2dlemstep  11235  fisumcom2  11239  fsumabs  11266  fsumiun  11278  binom  11285  bcxmas  11290  arisum  11299  expcnvap0  11303  explecnv  11306  geosergap  11307  geolim  11312  geolim2  11313  geo2sum  11315  geo2lim  11317  cvgratnnlemrate  11331  cvgratz  11333  mertenslemi1  11336  prodf1  11343  prodeq2w  11357  efcllemp  11401  ege2le3  11414  eftlub  11433  efgt1  11440  tanval2ap  11456  tanval3ap  11457  resinval  11458  recosval  11459  efi4p  11460  resin4p  11461  recos4p  11462  resincl  11463  recoscl  11464  efmival  11476  efeul  11477  sinadd  11479  cosadd  11480  tanaddap  11482  sinmul  11487  cos2tsin  11494  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  cos01gt0  11505  absef  11512  absefib  11513  efieq1re  11514  demoivreALT  11516  eirraplem  11519  odd2np1  11606  oddm1even  11608  oddp1even  11609  oexpneg  11610  opoe  11628  omoe  11629  nn0o1gt2  11638  nn0o  11640  algcvg  11765  algcvgblem  11766  1nprm  11831  1idssfct  11832  oddprmge3  11851  divgcdodd  11857  pw2dvdslemn  11879  pw2dvds  11880  oddpwdclemodd  11886  oddpwdc  11888  phicl2  11926  phibndlem  11928  phibnd  11929  hashdvds  11933  crth  11936  phimullem  11937  hashgcdeq  11940  evenennn  11942  ennnfonelemj0  11950  ennnfonelemjn  11951  ennnfonelemg  11952  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemnn0  11971  exmidunben  11975  ctinfomlemom  11976  slotex  12025  setscom  12038  setsslid  12048  2strbas1g  12102  2strop1g  12103  rngbaseg  12114  rngplusgg  12115  rngmulrg  12116  srngbased  12121  srngplusgd  12122  srngmulrd  12123  srnginvld  12124  lmodbased  12132  lmodplusgd  12133  lmodscad  12134  lmodvscad  12135  ipsbased  12140  ipsaddgd  12141  ipsmulrd  12142  ipsscad  12143  ipsvscad  12144  ipsipd  12145  topgrpbasd  12150  topgrpplusgd  12151  topgrptsetd  12152  toponsspwpwg  12228  topgele  12235  istps  12238  topontopn  12243  tgvalex  12258  tgclb  12273  lmfval  12400  lmres  12456  ispsmet  12531  psmetge0  12539  ismet  12552  isxmet  12553  xmetge0  12573  isxms2  12660  comet  12707  bdxmet  12709  cnmetdval  12737  cnbl0  12742  cnblcld  12743  reopnap  12746  tgioo  12754  cncfcncntop  12788  cncfmpt2fcntop  12793  limcimolemlt  12841  cnplimcim  12844  cnplimclemr  12846  limccnpcntop  12852  limccnp2lem  12853  limccnp2cntop  12854  dvfvalap  12858  dvbss  12862  dvcnp2cntop  12871  dvcn  12872  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvcjbr  12880  dvrecap  12885  dveflem  12895  reeff1olem  12900  pilem3  12912  ef2kpi  12935  efper  12936  sinperlem  12937  efimpi  12948  ptolemy  12953  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  sinq12gt0  12959  cosq14gt0  12961  tangtx  12967  sinkpi  12976  coskpi  12977  cosordlem  12978  rplogcl  13008  logge0  13009  logdivlti  13010  logbleb  13086  logblt  13087  pwf1oexmid  13367  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419