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  4070  unipw  4194  opeluu  4427  uniexb  4450  unon  4487  onintrab2im  4494  xpexg  4717  resiexg  4928  imaexg  4957  exse2  4977  soirri  4997  djudisj  5030  elxp5  5091  cnvexg  5140  cnviinm  5144  coexg  5147  funssres  5229  f1oabexg  5443  sefvex  5506  ssimaex  5546  mptfvex  5570  f1ompt  5635  fmptcof  5651  resfunexg  5705  mptexg  5709  funfvima3  5717  ovid  5954  ov  5957  ofres  6063  cofunexg  6076  opabex3d  6086  opabex3  6087  oprabexd  6092  1stcof  6128  2ndcof  6129  mpoexxg  6175  cnvf1o  6189  f2ndf  6190  algrflemg  6194  tposexg  6222  tfrlemisucaccv  6289  tfrlemibxssdm  6291  tfrlemibfn  6292  tfrlemi14d  6297  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfr1onlemres  6313  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllembfn  6321  tfrcllemres  6326  rdgtfr  6338  rdgruledefgg  6339  rdgon  6350  frecabex  6362  freccllem  6366  frecfcllem  6368  omcl  6425  oeicl  6426  erth  6541  th3qlem1  6599  mapex  6616  pmvalg  6621  mapsnconst  6656  ixpexgg  6684  fundmen  6768  cnvct  6771  snfig  6776  unen  6778  xpdom2  6793  mapxpen  6810  phplem2  6815  findcard2  6851  findcard2s  6852  infnfi  6857  relcnvfi  6902  sbthlemi8  6925  sbthlemi10  6927  fival  6931  fiss  6938  inl11  7026  casef  7049  caseinj  7050  caseinl  7052  caseinr  7053  djudom  7054  difinfsn  7061  djuinj  7067  0ct  7068  ctmlemr  7069  ctssdccl  7072  enomnilem  7098  enmkvlem  7121  enwomnilem  7129  djuassen  7169  xpdjuen  7170  djudoml  7171  djudomr  7172  cc2lem  7203  ltnnnq  7360  nnnq0lem1  7383  addnqprlemfl  7496  addnqprlemfu  7497  mulnqprlemfl  7512  mulnqprlemfu  7513  suplocexprlem2b  7651  prsrlem1  7679  gt0srpr  7685  caucvgsrlemcl  7726  caucvgsrlemfv  7728  caucvgsrlembound  7731  mulcnsr  7772  mulcnsrec  7780  addvalex  7781  pitoregt0  7786  axmulass  7810  axdistr  7811  recriota  7827  mulid1  7892  axmulgt0  7966  cnegexlem2  8070  cnegex  8072  gt0ne0d  8406  recexre  8472  msqge0  8510  mulge0  8513  recgt0  8741  recreclt  8791  cju  8852  nnge1  8876  nnnlt1  8879  nn0nlt0  9136  elz2  9258  nnm1ge0  9273  recnz  9280  zneo  9288  uz3m2nn  9507  eluz2b2  9537  nn01to3  9551  mnflt  9715  xnn0dcle  9734  xltadd1  9808  lincmb01cmp  9935  iccf1o  9936  fz1n  9975  fseq1p1m1  10025  fznn0  10044  fzctr  10064  4fvwrd4  10071  elfzonlteqm1  10141  divfl0  10227  modqelico  10265  zmodfz  10277  modqid  10280  modqmuladdim  10298  m1modge3gt1  10302  addmodid  10303  frec2uzf1od  10337  frecfzennn  10357  frecfzen2  10358  fzfig  10361  ser0  10445  ser3le  10449  expgt1  10489  expubnd  10508  iexpcyc  10555  binom2sub  10564  binom3  10568  zesq  10569  bernneq  10571  bernneq2  10572  expnbnd  10574  expnlbnd2  10576  facdiv  10647  faclbnd2  10651  faclbnd3  10652  bcval4  10661  hashinfom  10687  hashennn  10689  fihashf1rn  10698  isfinite4im  10702  hashfz  10730  crre  10795  crim  10796  remim  10798  mulreap  10802  cjreb  10804  recj  10805  reneg  10806  readd  10807  remullem  10809  imcj  10813  imneg  10814  imadd  10815  cjadd  10822  cjneg  10828  imval2  10832  cjreim  10841  cnrecnv  10848  uzin2  10925  absval  10939  rennim  10940  resqrexlemcalc3  10954  resqrexlemnm  10956  resqrexlemcvg  10957  resqrexlemgt0  10958  resqrexlemga  10961  absreimsq  11005  absreim  11006  amgm2  11056  climconst2  11228  climshft  11241  climshft2  11243  reccn2ap  11250  climge0  11262  sumsnf  11346  sumnul  11361  isumcl  11362  fsum2dlemstep  11371  fisumcom2  11375  fsumabs  11402  fsumiun  11414  binom  11421  bcxmas  11426  arisum  11435  expcnvap0  11439  explecnv  11442  geosergap  11443  geolim  11448  geolim2  11449  geo2sum  11451  geo2lim  11453  cvgratnnlemrate  11467  cvgratz  11469  mertenslemi1  11472  prodf1  11479  prodeq2w  11493  fprodntrivap  11521  prodsnf  11529  fprod2dlemstep  11559  fprodcom2fi  11563  efcllemp  11595  ege2le3  11608  eftlub  11627  efgt1  11634  tanval2ap  11650  tanval3ap  11651  resinval  11652  recosval  11653  efi4p  11654  resin4p  11655  recos4p  11656  resincl  11657  recoscl  11658  efmival  11670  efeul  11671  sinadd  11673  cosadd  11674  tanaddap  11676  sinmul  11681  cos2tsin  11688  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  sin01gt0  11698  cos01gt0  11699  absef  11706  absefib  11707  efieq1re  11708  demoivreALT  11710  eirraplem  11713  odd2np1  11806  oddm1even  11808  oddp1even  11809  oexpneg  11810  opoe  11828  omoe  11829  nn0o1gt2  11838  nn0o  11840  algcvg  11976  algcvgblem  11977  1nprm  12042  1idssfct  12043  oddprmge3  12063  divgcdodd  12071  pw2dvdslemn  12093  pw2dvds  12094  oddpwdclemodd  12100  oddpwdc  12102  phicl2  12142  phibndlem  12144  phibnd  12145  hashdvds  12149  crth  12152  phimullem  12153  eulerthlemfi  12156  eulerthlemrprm  12157  eulerthlema  12158  hashgcdeq  12167  phisum  12168  oddprm  12187  prm23ge5  12192  pythagtriplem1  12193  pythagtriplem4  12196  pythagtriplem12  12203  pythagtriplem14  12205  pczpre  12225  pcadd  12267  pcmpt  12269  pockthlem  12282  pockthi  12284  infpnlem2  12286  gzreim  12305  evenennn  12322  ennnfonelemj0  12330  ennnfonelemjn  12331  ennnfonelemg  12332  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemnn0  12351  exmidunben  12355  ctinfomlemom  12356  ssnnctlemct  12375  nninfdc  12382  slotex  12417  setscom  12430  setsslid  12440  2strbas1g  12494  2strop1g  12495  rngbaseg  12506  rngplusgg  12507  rngmulrg  12508  srngbased  12513  srngplusgd  12514  srngmulrd  12515  srnginvld  12516  lmodbased  12524  lmodplusgd  12525  lmodscad  12526  lmodvscad  12527  ipsbased  12532  ipsaddgd  12533  ipsmulrd  12534  ipsscad  12535  ipsvscad  12536  ipsipd  12537  topgrpbasd  12542  topgrpplusgd  12543  topgrptsetd  12544  toponsspwpwg  12620  topgele  12627  istps  12630  topontopn  12635  tgvalex  12650  tgclb  12665  lmfval  12792  lmres  12848  ispsmet  12923  psmetge0  12931  ismet  12944  isxmet  12945  xmetge0  12965  isxms2  13052  comet  13099  bdxmet  13101  cnmetdval  13129  cnbl0  13134  cnblcld  13135  reopnap  13138  tgioo  13146  cncfcncntop  13180  cncfmpt2fcntop  13185  limcimolemlt  13233  cnplimcim  13236  cnplimclemr  13238  limccnpcntop  13244  limccnp2lem  13245  limccnp2cntop  13246  dvfvalap  13250  dvbss  13254  dvcnp2cntop  13263  dvcn  13264  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvrecap  13277  dveflem  13287  reeff1olem  13292  pilem3  13304  ef2kpi  13327  efper  13328  sinperlem  13329  efimpi  13340  ptolemy  13345  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  cosq14gt0  13353  tangtx  13359  sinkpi  13368  coskpi  13369  cosordlem  13370  rplogcl  13400  logge0  13401  logdivlti  13402  logbleb  13479  logblt  13480  binom4  13497  lgsval2lem  13511  lgsval4a  13523  lgsneg  13525  lgsdilem  13528  lgsdirprm  13535  lgsdirnn0  13548  2sqlem2  13551  pwf1oexmid  13839  isomninnlem  13869  iswomninnlem  13888  ismkvnnlem  13891