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  4173  unipw  4304  opeluu  4542  uniexb  4565  unon  4604  onintrab2im  4611  xpexg  4835  resiexg  5053  imaexg  5085  exse2  5105  soirri  5126  djudisj  5159  elxp5  5220  cnvexg  5269  cnviinm  5273  coexg  5276  funssres  5363  f1oabexg  5589  sefvex  5653  ssimaex  5700  mptfvex  5725  f1ompt  5791  fmptcof  5807  resfunexg  5867  mptexg  5871  funfvima3  5880  ovid  6130  ov  6133  ofres  6242  cofunexg  6263  opabex3d  6275  opabex3  6276  oprabexd  6281  1stcof  6318  2ndcof  6319  mpoexxg  6367  cnvf1o  6382  f2ndf  6383  algrflemg  6387  tposexg  6415  tfrlemisucaccv  6482  tfrlemibxssdm  6484  tfrlemibfn  6485  tfrlemi14d  6490  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfr1onlembfn  6501  tfr1onlemres  6506  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllembfn  6514  tfrcllemres  6519  rdgtfr  6531  rdgruledefgg  6532  rdgon  6543  frecabex  6555  freccllem  6559  frecfcllem  6561  omcl  6620  oeicl  6621  erth  6739  th3qlem1  6797  mapex  6814  pmvalg  6819  mapsnconst  6854  ixpexgg  6882  fundmen  6972  cnvct  6975  snfig  6980  unen  6982  xpdom2  7003  mapxpen  7022  phplem2  7027  findcard2  7064  findcard2s  7065  infnfi  7070  relcnvfi  7124  sbthlemi8  7147  sbthlemi10  7149  fival  7153  fiss  7160  inl11  7248  casef  7271  caseinj  7272  caseinl  7274  caseinr  7275  djudom  7276  difinfsn  7283  djuinj  7289  0ct  7290  ctmlemr  7291  ctssdccl  7294  enomnilem  7321  enmkvlem  7344  enwomnilem  7352  djuassen  7415  xpdjuen  7416  djudoml  7417  djudomr  7418  cc2lem  7468  ltnnnq  7626  nnnq0lem1  7649  addnqprlemfl  7762  addnqprlemfu  7763  mulnqprlemfl  7778  mulnqprlemfu  7779  suplocexprlem2b  7917  prsrlem1  7945  gt0srpr  7951  caucvgsrlemcl  7992  caucvgsrlemfv  7994  caucvgsrlembound  7997  mulcnsr  8038  mulcnsrec  8046  addvalex  8047  pitoregt0  8052  axmulass  8076  axdistr  8077  recriota  8093  mulrid  8159  axmulgt0  8234  cnegexlem2  8338  cnegex  8340  gt0ne0d  8675  recexre  8741  msqge0  8779  mulge0  8782  aptap  8813  recgt0  9013  recreclt  9063  cju  9124  nnge1  9149  nnnlt1  9152  nn0nlt0  9411  nnnle0  9511  elz2  9534  nnm1ge0  9549  recnz  9556  zneo  9564  uz3m2nn  9785  eluz2b2  9815  nn01to3  9829  mnflt  9996  xnn0dcle  10015  xltadd1  10089  lincmb01cmp  10216  iccf1o  10217  fz1n  10257  fseq1p1m1  10307  fznn0  10326  fzctr  10346  4fvwrd4  10353  fzo0n  10381  elfzonlteqm1  10433  divfl0  10533  modqelico  10573  zmodfz  10585  modqid  10588  modqmuladdim  10606  m1modge3gt1  10610  addmodid  10611  frec2uzf1od  10645  frecfzennn  10665  frecfzen2  10666  fzfig  10669  ser0  10772  ser3le  10776  expgt1  10816  expubnd  10835  iexpcyc  10883  binom2sub  10892  binom3  10896  zesq  10897  bernneq  10899  bernneq2  10900  expnbnd  10902  expnlbnd2  10904  facdiv  10977  faclbnd2  10981  faclbnd3  10982  bcval4  10991  hashinfom  11017  hashennn  11019  fihashf1rn  11027  isfinite4im  11031  hashfz  11061  iswrd  11091  iswrdiz  11096  wrdexg  11100  wrdexb  11101  wrdfin  11108  wrdnval  11120  wrdred1hash  11133  ccatsymb  11155  ccatalpha  11166  s111  11184  fzowrddc  11200  swrdlen  11205  swrdwrdsymbg  11217  pfxval  11227  pfx0g  11229  fnpfx  11230  pfxlen  11238  cats1un  11274  swrdccat  11288  crre  11389  crim  11390  remim  11392  mulreap  11396  cjreb  11398  recj  11399  reneg  11400  readd  11401  remullem  11403  imcj  11407  imneg  11408  imadd  11409  cjadd  11416  cjneg  11422  imval2  11426  cjreim  11435  cnrecnv  11442  uzin2  11519  absval  11533  rennim  11534  resqrexlemcalc3  11548  resqrexlemnm  11550  resqrexlemcvg  11551  resqrexlemgt0  11552  resqrexlemga  11555  absreimsq  11599  absreim  11600  amgm2  11650  climconst2  11823  climshft  11836  climshft2  11838  reccn2ap  11845  climge0  11857  sumsnf  11941  sumnul  11956  isumcl  11957  fsum2dlemstep  11966  fisumcom2  11970  fsumabs  11997  fsumiun  12009  binom  12016  bcxmas  12021  arisum  12030  expcnvap0  12034  explecnv  12037  geosergap  12038  geolim  12043  geolim2  12044  geo2sum  12046  geo2lim  12048  cvgratnnlemrate  12062  cvgratz  12064  mertenslemi1  12067  prodf1  12074  prodeq2w  12088  fprodntrivap  12116  prodsnf  12124  fprod2dlemstep  12154  fprodcom2fi  12158  efcllemp  12190  ege2le3  12203  eftlub  12222  efgt1  12229  tanval2ap  12245  tanval3ap  12246  resinval  12247  recosval  12248  efi4p  12249  resin4p  12250  recos4p  12251  resincl  12252  recoscl  12253  efmival  12265  efeul  12266  sinadd  12268  cosadd  12269  tanaddap  12271  sinmul  12276  cos2tsin  12283  ef01bndlem  12288  sin01bnd  12289  cos01bnd  12290  sin01gt0  12294  cos01gt0  12295  absef  12302  absefib  12303  efieq1re  12304  demoivreALT  12306  eirraplem  12309  3dvds  12396  odd2np1  12405  oddm1even  12407  oddp1even  12408  oexpneg  12409  opoe  12427  omoe  12428  nn0o1gt2  12437  nn0o  12439  bitsdc  12479  bitsfzolem  12486  bitsfzo  12487  bitsinv1lem  12493  bitsinv1  12494  nninfctlemfo  12582  algcvg  12591  algcvgblem  12592  1nprm  12657  1idssfct  12658  oddprmge3  12678  divgcdodd  12686  pw2dvdslemn  12708  pw2dvds  12709  oddpwdclemodd  12715  oddpwdc  12717  phicl2  12757  phibndlem  12759  phibnd  12760  hashdvds  12764  crth  12767  phimullem  12768  eulerthlemfi  12771  eulerthlemrprm  12772  eulerthlema  12773  hashgcdeq  12783  phisum  12784  oddprm  12803  prm23ge5  12808  pythagtriplem1  12809  pythagtriplem4  12812  pythagtriplem12  12819  pythagtriplem14  12821  pczpre  12841  pcadd  12884  pcmpt  12887  pockthlem  12900  pockthi  12902  infpnlem2  12904  gzreim  12923  4sqlem11  12945  4sqlem12  12946  4sqlem13m  12947  4sqlem17  12951  2expltfac  12983  evenennn  12985  ennnfonelemjn  12994  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemex  13006  ennnfonelemhom  13007  ennnfonelemnn0  13014  exmidunben  13018  ctinfomlemom  13019  ssnnctlemct  13038  nninfdc  13045  slotex  13080  setscom  13093  strslfv3  13099  setsslid  13104  bassetsnn  13110  basmex  13113  basmexd  13114  relelbasov  13116  ressbas2d  13122  ressbasid  13124  strressid  13125  ressval3d  13126  2strbas1g  13177  2strop1g  13178  rngbaseg  13190  rngplusgg  13191  rngmulrg  13192  srngbased  13201  srngplusgd  13202  srngmulrd  13203  srnginvld  13204  lmodbased  13219  lmodplusgd  13220  lmodscad  13221  lmodvscad  13222  ipsbased  13231  ipsaddgd  13232  ipsmulrd  13233  ipsscad  13234  ipsvscad  13235  ipsipd  13236  topgrpbasd  13251  topgrpplusgd  13252  topgrptsetd  13253  tgvalex  13317  prdsex  13323  prdsval  13327  prdsbaslemss  13328  prdsbas  13330  prdsplusg  13331  prdsmulr  13332  pwsbas  13346  pwselbasb  13347  pwssnf1o  13352  imasex  13359  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfn  13371  imasaddval  13372  imasaddf  13373  imasmulfn  13374  imasmulval  13375  imasmulf  13376  qusval  13377  qusex  13379  qusaddvallemg  13387  qusaddflemg  13388  qusaddval  13389  qusaddf  13390  qusmulval  13391  qusmulf  13392  xpsfval  13402  xpsval  13406  plusffvalg  13416  grpidvalg  13427  igsumvalx  13443  gsumfzval  13445  gsumress  13449  gsum0g  13450  gsumval2  13451  issubmnd  13496  ress0g  13497  ismhm  13515  mhmex  13516  issubm  13526  0mhm  13540  grppropstrg  13573  grpinvfvalg  13596  grpinvval  13597  grpinvfng  13598  grpsubfvalg  13599  grpsubval  13600  grpressid  13615  grplactfval  13655  qusgrp2  13671  mulgfvalg  13679  mulgex  13681  mulgnngsum  13685  issubg  13731  subgex  13734  subgmulg  13746  issubg2m  13747  releqgg  13778  eqgex  13779  eqgfval  13780  eqgen  13785  isghm  13801  ablressid  13893  mgptopng  13913  rngressid  13938  qusrng  13942  dfur2g  13946  ringidss  14013  ring1  14043  ringressid  14047  qusring2  14050  dvdsrvald  14078  dvdsrex  14083  unitgrp  14101  unitabl  14102  invrfvald  14107  unitlinv  14111  unitrinv  14112  dvrfvald  14118  rdivmuldivd  14129  invrpropdg  14134  rhmunitinv  14163  isnzr2  14169  issubrng  14184  issubrg  14206  subrgugrp  14225  subrgpropd  14238  rrgmex  14246  aprval  14267  islmod  14276  scaffvalg  14291  lssex  14339  lssmex  14340  lsssetm  14341  islssmg  14343  islss3  14364  lspfval  14373  lspval  14375  lspcl  14376  lspex  14380  sralemg  14423  srascag  14427  sravscag  14428  sraipg  14429  sraex  14431  rlmsubg  14443  rlmvnegg  14450  ixpsnbasval  14451  lidlvalg  14456  rspvalg  14457  lidlex  14458  rspex  14459  lidlmex  14460  lidlss  14461  lidlrsppropdg  14480  2idlmex  14486  qusrhm  14513  znlidl  14619  zncrng2  14620  znval  14621  znle  14622  znbaslemnn  14624  znbas  14629  znzrh2  14631  znzrhval  14632  znzrhfo  14633  zndvds  14634  znfi  14640  znhash  14641  znidom  14642  znidomb  14643  psrval  14651  psrbasg  14659  psrelbas  14660  psrplusgg  14663  psraddcl  14665  psr0cl  14666  psrnegcl  14668  psr1clfi  14673  mplvalcoe  14675  mplplusgg  14688  toponsspwpwg  14717  topgele  14724  istps  14727  topontopn  14732  tgclb  14760  lmfval  14888  lmres  14943  ispsmet  15018  psmetge0  15026  ismet  15039  isxmet  15040  xmetge0  15060  isxms2  15147  comet  15194  bdxmet  15196  cnmetdval  15224  cnbl0  15229  cnblcld  15230  reopnap  15241  tgioo  15249  cncfcncntop  15288  cncfmpt2fcntop  15294  maxcncf  15310  mincncf  15311  hovergt0  15345  limcimolemlt  15359  cnplimcim  15362  cnplimclemr  15364  limccnpcntop  15370  limccnp2lem  15371  limccnp2cntop  15372  dvfvalap  15376  dvbss  15380  dvcnp2cntop  15394  dvcn  15395  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvcjbr  15403  dvrecap  15408  dvmptfsum  15420  dveflem  15421  plyval  15427  plycolemc  15453  dvply2  15462  reeff1olem  15466  pilem3  15478  ef2kpi  15501  efper  15502  sinperlem  15503  efimpi  15514  ptolemy  15519  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  sinq12gt0  15525  cosq14gt0  15527  tangtx  15533  sinkpi  15542  coskpi  15543  cosordlem  15544  rplogcl  15574  logge0  15575  logdivlti  15576  logbleb  15656  logblt  15657  binom4  15674  wilthlem1  15675  1sgmprm  15689  1sgm2ppw  15690  mersenne  15692  perfect1  15693  perfectlem1  15694  perfectlem2  15695  perfect  15696  lgsval2lem  15710  lgsval4a  15722  lgsneg  15724  lgsdilem  15727  lgsdirprm  15734  lgsdirnn0  15747  gausslemma2dlem0i  15757  gausslemma2dlem6  15767  gausslemma2dlem7  15768  gausslemma2d  15769  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem3  15772  lgseisenlem4  15773  lgsquadlemofi  15776  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad2lem2  15782  lgsquad2  15783  m1lgs  15785  2lgs  15804  2lgsoddprmlem2  15806  2lgsoddprm  15813  2sqlem2  15815  vtxvalg  15838  vtxex  15840  struct2slots2dom  15860  structvtxval  15861  structiedg0val  15862  structgrssvtx  15864  structgrssiedg  15865  edgstruct  15885  wlkv0  16141  upgr2wlkdc  16147  clwwlkex  16167  clwwlkccatlem  16169  pwf1oexmid  16478  nnnninfex  16502  isomninnlem  16512  iswomninnlem  16531  ismkvnnlem  16534