Theorem sylancr 410

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 408	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  4017  unipw  4139  opeluu  4371  uniexb  4394  unon  4427  onintrab2im  4434  xpexg  4653  resiexg  4864  imaexg  4893  exse2  4913  soirri  4933  djudisj  4966  elxp5  5027  cnvexg  5076  cnviinm  5080  coexg  5083  funssres  5165  f1oabexg  5379  sefvex  5442  ssimaex  5482  mptfvex  5506  f1ompt  5571  fmptcof  5587  resfunexg  5641  mptexg  5645  funfvima3  5651  ovid  5887  ov  5890  ofres  5996  cofunexg  6009  opabex3d  6019  opabex3  6020  oprabexd  6025  1stcof  6061  2ndcof  6062  mpoexxg  6108  cnvf1o  6122  f2ndf  6123  algrflemg  6127  tposexg  6155  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemi14d  6230  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemres  6246  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemres  6259  rdgtfr  6271  rdgruledefgg  6272  rdgon  6283  frecabex  6295  freccllem  6299  frecfcllem  6301  omcl  6357  oeicl  6358  erth  6473  th3qlem1  6531  mapex  6548  pmvalg  6553  mapsnconst  6588  ixpexgg  6616  fundmen  6700  cnvct  6703  snfig  6708  unen  6710  xpdom2  6725  mapxpen  6742  phplem2  6747  findcard2  6783  findcard2s  6784  infnfi  6789  relcnvfi  6829  sbthlemi8  6852  sbthlemi10  6854  fival  6858  fiss  6865  inl11  6950  casef  6973  caseinj  6974  caseinl  6976  caseinr  6977  djudom  6978  difinfsn  6985  djuinj  6991  0ct  6992  ctmlemr  6993  ctssdccl  6996  enomnilem  7010  djuassen  7073  xpdjuen  7074  djudoml  7075  djudomr  7076  ltnnnq  7231  nnnq0lem1  7254  addnqprlemfl  7367  addnqprlemfu  7368  mulnqprlemfl  7383  mulnqprlemfu  7384  suplocexprlem2b  7522  prsrlem1  7550  gt0srpr  7556  caucvgsrlemcl  7597  caucvgsrlemfv  7599  caucvgsrlembound  7602  mulcnsr  7643  mulcnsrec  7651  addvalex  7652  pitoregt0  7657  axmulass  7681  axdistr  7682  recriota  7698  mulid1  7763  axmulgt0  7836  cnegexlem2  7938  cnegex  7940  gt0ne0d  8274  recexre  8340  msqge0  8378  mulge0  8381  recgt0  8608  recreclt  8658  cju  8719  nnge1  8743  nnnlt1  8746  nn0nlt0  9003  elz2  9122  nnm1ge0  9137  recnz  9144  zneo  9152  uz3m2nn  9368  eluz2b2  9397  nn01to3  9409  mnflt  9569  xltadd1  9659  lincmb01cmp  9786  iccf1o  9787  fz1n  9824  fseq1p1m1  9874  fznn0  9893  fzctr  9910  4fvwrd4  9917  elfzonlteqm1  9987  divfl0  10069  modqelico  10107  zmodfz  10119  modqid  10122  modqmuladdim  10140  m1modge3gt1  10144  addmodid  10145  frec2uzf1od  10179  frecfzennn  10199  frecfzen2  10200  fzfig  10203  ser0  10287  ser3le  10291  expgt1  10331  expubnd  10350  iexpcyc  10397  binom2sub  10405  binom3  10409  zesq  10410  bernneq  10412  bernneq2  10413  expnbnd  10415  expnlbnd2  10417  facdiv  10484  faclbnd2  10488  faclbnd3  10489  bcval4  10498  hashinfom  10524  hashennn  10526  fihashf1rn  10535  isfinite4im  10539  hashfz  10567  crre  10629  crim  10630  remim  10632  mulreap  10636  cjreb  10638  recj  10639  reneg  10640  readd  10641  remullem  10643  imcj  10647  imneg  10648  imadd  10649  cjadd  10656  cjneg  10662  imval2  10666  cjreim  10675  cnrecnv  10682  uzin2  10759  absval  10773  rennim  10774  resqrexlemcalc3  10788  resqrexlemnm  10790  resqrexlemcvg  10791  resqrexlemgt0  10792  resqrexlemga  10795  absreimsq  10839  absreim  10840  amgm2  10890  climconst2  11060  climshft  11073  climshft2  11075  reccn2ap  11082  climge0  11094  sumsnf  11178  sumnul  11193  isumcl  11194  fsum2dlemstep  11203  fisumcom2  11207  fsumabs  11234  fsumiun  11246  binom  11253  bcxmas  11258  arisum  11267  expcnvap0  11271  explecnv  11274  geosergap  11275  geolim  11280  geolim2  11281  geo2sum  11283  geo2lim  11285  cvgratnnlemrate  11299  cvgratz  11301  mertenslemi1  11304  prodf1  11311  prodeq2w  11325  efcllemp  11364  ege2le3  11377  eftlub  11396  efgt1  11403  tanval2ap  11420  tanval3ap  11421  resinval  11422  recosval  11423  efi4p  11424  resin4p  11425  recos4p  11426  resincl  11427  recoscl  11428  efmival  11440  efeul  11441  sinadd  11443  cosadd  11444  tanaddap  11446  sinmul  11451  cos2tsin  11458  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  cos01gt0  11469  absef  11476  absefib  11477  efieq1re  11478  demoivreALT  11480  eirraplem  11483  odd2np1  11570  oddm1even  11572  oddp1even  11573  oexpneg  11574  opoe  11592  omoe  11593  nn0o1gt2  11602  nn0o  11604  algcvg  11729  algcvgblem  11730  1nprm  11795  1idssfct  11796  oddprmge3  11815  divgcdodd  11821  pw2dvdslemn  11843  pw2dvds  11844  oddpwdclemodd  11850  oddpwdc  11852  phicl2  11890  phibndlem  11892  phibnd  11893  hashdvds  11897  crth  11900  phimullem  11901  hashgcdeq  11904  evenennn  11906  ennnfonelemj0  11914  ennnfonelemjn  11915  ennnfonelemg  11916  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemnn0  11935  exmidunben  11939  ctinfomlemom  11940  slotex  11986  setscom  11999  setsslid  12009  2strbas1g  12063  2strop1g  12064  rngbaseg  12075  rngplusgg  12076  rngmulrg  12077  srngbased  12082  srngplusgd  12083  srngmulrd  12084  srnginvld  12085  lmodbased  12093  lmodplusgd  12094  lmodscad  12095  lmodvscad  12096  ipsbased  12101  ipsaddgd  12102  ipsmulrd  12103  ipsscad  12104  ipsvscad  12105  ipsipd  12106  topgrpbasd  12111  topgrpplusgd  12112  topgrptsetd  12113  toponsspwpwg  12189  topgele  12196  istps  12199  topontopn  12204  tgvalex  12219  tgclb  12234  lmfval  12361  lmres  12417  ispsmet  12492  psmetge0  12500  ismet  12513  isxmet  12514  xmetge0  12534  isxms2  12621  comet  12668  bdxmet  12670  cnmetdval  12698  cnbl0  12703  cnblcld  12704  reopnap  12707  tgioo  12715  cncfcncntop  12749  cncfmpt2fcntop  12754  limcimolemlt  12802  cnplimcim  12805  cnplimclemr  12807  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  dvfvalap  12819  dvbss  12823  dvcnp2cntop  12832  dvcn  12833  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvcjbr  12841  dvrecap  12846  dveflem  12855  pilem3  12864  ef2kpi  12887  efper  12888  sinperlem  12889  efimpi  12900  ptolemy  12905  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  sinq12gt0  12911  cosq14gt0  12913  tangtx  12919  sinkpi  12928  coskpi  12929  cosordlem  12930  pwf1oexmid  13194  isomninnlem  13225