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  4138  unipw  4266  opeluu  4502  uniexb  4525  unon  4564  onintrab2im  4571  xpexg  4794  resiexg  5010  imaexg  5042  exse2  5062  soirri  5083  djudisj  5116  elxp5  5177  cnvexg  5226  cnviinm  5230  coexg  5233  funssres  5319  f1oabexg  5543  sefvex  5607  ssimaex  5650  mptfvex  5675  f1ompt  5741  fmptcof  5757  resfunexg  5815  mptexg  5819  funfvima3  5828  ovid  6072  ov  6075  ofres  6183  cofunexg  6204  opabex3d  6216  opabex3  6217  oprabexd  6222  1stcof  6259  2ndcof  6260  mpoexxg  6306  cnvf1o  6321  f2ndf  6322  algrflemg  6326  tposexg  6354  tfrlemisucaccv  6421  tfrlemibxssdm  6423  tfrlemibfn  6424  tfrlemi14d  6429  tfr1onlemsucaccv  6437  tfr1onlembxssdm  6439  tfr1onlembfn  6440  tfr1onlemres  6445  tfrcllemsucaccv  6450  tfrcllembxssdm  6452  tfrcllembfn  6453  tfrcllemres  6458  rdgtfr  6470  rdgruledefgg  6471  rdgon  6482  frecabex  6494  freccllem  6498  frecfcllem  6500  omcl  6557  oeicl  6558  erth  6676  th3qlem1  6734  mapex  6751  pmvalg  6756  mapsnconst  6791  ixpexgg  6819  fundmen  6909  cnvct  6912  snfig  6917  unen  6919  xpdom2  6938  mapxpen  6957  phplem2  6962  findcard2  6998  findcard2s  6999  infnfi  7004  relcnvfi  7055  sbthlemi8  7078  sbthlemi10  7080  fival  7084  fiss  7091  inl11  7179  casef  7202  caseinj  7203  caseinl  7205  caseinr  7206  djudom  7207  difinfsn  7214  djuinj  7220  0ct  7221  ctmlemr  7222  ctssdccl  7225  enomnilem  7252  enmkvlem  7275  enwomnilem  7283  djuassen  7342  xpdjuen  7343  djudoml  7344  djudomr  7345  cc2lem  7391  ltnnnq  7549  nnnq0lem1  7572  addnqprlemfl  7685  addnqprlemfu  7686  mulnqprlemfl  7701  mulnqprlemfu  7702  suplocexprlem2b  7840  prsrlem1  7868  gt0srpr  7874  caucvgsrlemcl  7915  caucvgsrlemfv  7917  caucvgsrlembound  7920  mulcnsr  7961  mulcnsrec  7969  addvalex  7970  pitoregt0  7975  axmulass  7999  axdistr  8000  recriota  8016  mulrid  8082  axmulgt0  8157  cnegexlem2  8261  cnegex  8263  gt0ne0d  8598  recexre  8664  msqge0  8702  mulge0  8705  aptap  8736  recgt0  8936  recreclt  8986  cju  9047  nnge1  9072  nnnlt1  9075  nn0nlt0  9334  nnnle0  9434  elz2  9457  nnm1ge0  9472  recnz  9479  zneo  9487  uz3m2nn  9707  eluz2b2  9737  nn01to3  9751  mnflt  9918  xnn0dcle  9937  xltadd1  10011  lincmb01cmp  10138  iccf1o  10139  fz1n  10179  fseq1p1m1  10229  fznn0  10248  fzctr  10268  4fvwrd4  10275  fzo0n  10303  elfzonlteqm1  10352  divfl0  10452  modqelico  10492  zmodfz  10504  modqid  10507  modqmuladdim  10525  m1modge3gt1  10529  addmodid  10530  frec2uzf1od  10564  frecfzennn  10584  frecfzen2  10585  fzfig  10588  ser0  10691  ser3le  10695  expgt1  10735  expubnd  10754  iexpcyc  10802  binom2sub  10811  binom3  10815  zesq  10816  bernneq  10818  bernneq2  10819  expnbnd  10821  expnlbnd2  10823  facdiv  10896  faclbnd2  10900  faclbnd3  10901  bcval4  10910  hashinfom  10936  hashennn  10938  fihashf1rn  10946  isfinite4im  10950  hashfz  10979  iswrd  11009  iswrdiz  11014  wrdexg  11018  wrdexb  11019  wrdfin  11026  wrdnval  11037  wrdred1hash  11050  ccatsymb  11072  s111  11099  fzowrddc  11114  swrdlen  11119  swrdwrdsymbg  11131  pfxval  11141  pfx0g  11143  pfxlen  11150  crre  11218  crim  11219  remim  11221  mulreap  11225  cjreb  11227  recj  11228  reneg  11229  readd  11230  remullem  11232  imcj  11236  imneg  11237  imadd  11238  cjadd  11245  cjneg  11251  imval2  11255  cjreim  11264  cnrecnv  11271  uzin2  11348  absval  11362  rennim  11363  resqrexlemcalc3  11377  resqrexlemnm  11379  resqrexlemcvg  11380  resqrexlemgt0  11381  resqrexlemga  11384  absreimsq  11428  absreim  11429  amgm2  11479  climconst2  11652  climshft  11665  climshft2  11667  reccn2ap  11674  climge0  11686  sumsnf  11770  sumnul  11785  isumcl  11786  fsum2dlemstep  11795  fisumcom2  11799  fsumabs  11826  fsumiun  11838  binom  11845  bcxmas  11850  arisum  11859  expcnvap0  11863  explecnv  11866  geosergap  11867  geolim  11872  geolim2  11873  geo2sum  11875  geo2lim  11877  cvgratnnlemrate  11891  cvgratz  11893  mertenslemi1  11896  prodf1  11903  prodeq2w  11917  fprodntrivap  11945  prodsnf  11953  fprod2dlemstep  11983  fprodcom2fi  11987  efcllemp  12019  ege2le3  12032  eftlub  12051  efgt1  12058  tanval2ap  12074  tanval3ap  12075  resinval  12076  recosval  12077  efi4p  12078  resin4p  12079  recos4p  12080  resincl  12081  recoscl  12082  efmival  12094  efeul  12095  sinadd  12097  cosadd  12098  tanaddap  12100  sinmul  12105  cos2tsin  12112  ef01bndlem  12117  sin01bnd  12118  cos01bnd  12119  sin01gt0  12123  cos01gt0  12124  absef  12131  absefib  12132  efieq1re  12133  demoivreALT  12135  eirraplem  12138  3dvds  12225  odd2np1  12234  oddm1even  12236  oddp1even  12237  oexpneg  12238  opoe  12256  omoe  12257  nn0o1gt2  12266  nn0o  12268  bitsdc  12308  bitsfzolem  12315  bitsfzo  12316  bitsinv1lem  12322  bitsinv1  12323  nninfctlemfo  12411  algcvg  12420  algcvgblem  12421  1nprm  12486  1idssfct  12487  oddprmge3  12507  divgcdodd  12515  pw2dvdslemn  12537  pw2dvds  12538  oddpwdclemodd  12544  oddpwdc  12546  phicl2  12586  phibndlem  12588  phibnd  12589  hashdvds  12593  crth  12596  phimullem  12597  eulerthlemfi  12600  eulerthlemrprm  12601  eulerthlema  12602  hashgcdeq  12612  phisum  12613  oddprm  12632  prm23ge5  12637  pythagtriplem1  12638  pythagtriplem4  12641  pythagtriplem12  12648  pythagtriplem14  12650  pczpre  12670  pcadd  12713  pcmpt  12716  pockthlem  12729  pockthi  12731  infpnlem2  12733  gzreim  12752  4sqlem11  12774  4sqlem12  12775  4sqlem13m  12776  4sqlem17  12780  2expltfac  12812  evenennn  12814  ennnfonelemjn  12823  ennnfonelemkh  12833  ennnfonelemhf1o  12834  ennnfonelemex  12835  ennnfonelemhom  12836  ennnfonelemnn0  12843  exmidunben  12847  ctinfomlemom  12848  ssnnctlemct  12867  nninfdc  12874  slotex  12909  setscom  12922  strslfv3  12928  setsslid  12933  basmex  12941  basmexd  12942  relelbasov  12944  ressbas2d  12950  ressbasid  12952  strressid  12953  ressval3d  12954  2strbas1g  13005  2strop1g  13006  rngbaseg  13018  rngplusgg  13019  rngmulrg  13020  srngbased  13029  srngplusgd  13030  srngmulrd  13031  srnginvld  13032  lmodbased  13047  lmodplusgd  13048  lmodscad  13049  lmodvscad  13050  ipsbased  13059  ipsaddgd  13060  ipsmulrd  13061  ipsscad  13062  ipsvscad  13063  ipsipd  13064  topgrpbasd  13079  topgrpplusgd  13080  topgrptsetd  13081  tgvalex  13145  prdsex  13151  prdsval  13155  prdsbaslemss  13156  prdsbas  13158  prdsplusg  13159  prdsmulr  13160  pwsbas  13174  pwselbasb  13175  pwssnf1o  13180  imasex  13187  imasival  13188  imasbas  13189  imasplusg  13190  imasmulr  13191  imasaddfn  13199  imasaddval  13200  imasaddf  13201  imasmulfn  13202  imasmulval  13203  imasmulf  13204  qusval  13205  qusex  13207  qusaddvallemg  13215  qusaddflemg  13216  qusaddval  13217  qusaddf  13218  qusmulval  13219  qusmulf  13220  xpsfval  13230  xpsval  13234  plusffvalg  13244  grpidvalg  13255  igsumvalx  13271  gsumfzval  13273  gsumress  13277  gsum0g  13278  gsumval2  13279  issubmnd  13324  ress0g  13325  ismhm  13343  mhmex  13344  issubm  13354  0mhm  13368  grppropstrg  13401  grpinvfvalg  13424  grpinvval  13425  grpinvfng  13426  grpsubfvalg  13427  grpsubval  13428  grpressid  13443  grplactfval  13483  qusgrp2  13499  mulgfvalg  13507  mulgex  13509  mulgnngsum  13513  issubg  13559  subgex  13562  subgmulg  13574  issubg2m  13575  releqgg  13606  eqgex  13607  eqgfval  13608  eqgen  13613  isghm  13629  ablressid  13721  mgptopng  13741  rngressid  13766  qusrng  13770  dfur2g  13774  ringidss  13841  ring1  13871  ringressid  13875  qusring2  13878  reldvdsrsrg  13904  dvdsrvald  13905  dvdsrex  13910  unitgrp  13928  unitabl  13929  invrfvald  13934  unitlinv  13938  unitrinv  13939  dvrfvald  13945  rdivmuldivd  13956  invrpropdg  13961  rhmunitinv  13990  isnzr2  13996  issubrng  14011  issubrg  14033  subrgugrp  14052  subrgpropd  14065  rrgmex  14073  aprval  14094  islmod  14103  scaffvalg  14118  lssex  14166  lssmex  14167  lsssetm  14168  islssmg  14170  islss3  14191  lspfval  14200  lspval  14202  lspcl  14203  lspex  14207  sralemg  14250  srascag  14254  sravscag  14255  sraipg  14256  sraex  14258  rlmsubg  14270  rlmvnegg  14277  ixpsnbasval  14278  lidlvalg  14283  rspvalg  14284  lidlex  14285  rspex  14286  lidlmex  14287  lidlss  14288  lidlrsppropdg  14307  2idlmex  14313  qusrhm  14340  znlidl  14446  zncrng2  14447  znval  14448  znle  14449  znbaslemnn  14451  znbas  14456  znzrh2  14458  znzrhval  14459  znzrhfo  14460  zndvds  14461  znfi  14467  znhash  14468  znidom  14469  znidomb  14470  psrval  14478  psrbasg  14486  psrelbas  14487  psrplusgg  14490  psraddcl  14492  psr0cl  14493  psrnegcl  14495  psr1clfi  14500  mplvalcoe  14502  mplplusgg  14515  toponsspwpwg  14544  topgele  14551  istps  14554  topontopn  14559  tgclb  14587  lmfval  14714  lmres  14770  ispsmet  14845  psmetge0  14853  ismet  14866  isxmet  14867  xmetge0  14887  isxms2  14974  comet  15021  bdxmet  15023  cnmetdval  15051  cnbl0  15056  cnblcld  15057  reopnap  15068  tgioo  15076  cncfcncntop  15115  cncfmpt2fcntop  15121  maxcncf  15137  mincncf  15138  hovergt0  15172  limcimolemlt  15186  cnplimcim  15189  cnplimclemr  15191  limccnpcntop  15197  limccnp2lem  15198  limccnp2cntop  15199  dvfvalap  15203  dvbss  15207  dvcnp2cntop  15221  dvcn  15222  dvaddxxbr  15223  dvmulxxbr  15224  dvcoapbr  15229  dvcjbr  15230  dvrecap  15235  dvmptfsum  15247  dveflem  15248  plyval  15254  plycolemc  15280  dvply2  15289  reeff1olem  15293  pilem3  15305  ef2kpi  15328  efper  15329  sinperlem  15330  efimpi  15341  ptolemy  15346  sincosq2sgn  15349  sincosq3sgn  15350  sincosq4sgn  15351  sinq12gt0  15352  cosq14gt0  15354  tangtx  15360  sinkpi  15369  coskpi  15370  cosordlem  15371  rplogcl  15401  logge0  15402  logdivlti  15403  logbleb  15483  logblt  15484  binom4  15501  wilthlem1  15502  1sgmprm  15516  1sgm2ppw  15517  mersenne  15519  perfect1  15520  perfectlem1  15521  perfectlem2  15522  perfect  15523  lgsval2lem  15537  lgsval4a  15549  lgsneg  15551  lgsdilem  15554  lgsdirprm  15561  lgsdirnn0  15574  gausslemma2dlem0i  15584  gausslemma2dlem6  15594  gausslemma2dlem7  15595  gausslemma2d  15596  lgseisenlem1  15597  lgseisenlem2  15598  lgseisenlem3  15599  lgseisenlem4  15600  lgsquadlemofi  15603  lgsquadlem1  15604  lgsquadlem2  15605  lgsquadlem3  15606  lgsquad2lem2  15609  lgsquad2  15610  m1lgs  15612  2lgs  15631  2lgsoddprmlem2  15633  2lgsoddprm  15640  2sqlem2  15642  vtxvalg  15665  vtxex  15667  struct2slots2dom  15687  structvtxval  15688  structiedg0val  15689  structgrssvtx  15691  structgrssiedg  15692  edgstruct  15710  pwf1oexmid  16051  nnnninfex  16074  isomninnlem  16084  iswomninnlem  16103  ismkvnnlem  16106