Theorem sylancr 418

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpteq2da  4220  unipw  4357  opeluu  4596  uniexb  4619  unon  4658  onintrab2im  4665  xpexg  4889  resiexg  5108  imaexg  5140  exse2  5161  soirri  5182  djudisj  5215  elxp5  5276  cnvexg  5325  cnviinm  5329  coexg  5332  funssres  5420  f1oabexg  5651  sefvex  5716  ssimaex  5764  mptfvex  5791  f1ompt  5859  fmptcof  5875  resfunexg  5936  mptexg  5942  funfvima3  5952  ovid  6205  ov  6208  ofres  6317  cofunexg  6338  opabex3d  6350  opabex3  6351  oprabexd  6360  1stcof  6397  2ndcof  6398  mpoexxg  6446  cnvf1o  6461  f2ndf  6462  algrflemg  6466  tposexg  6529  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi14d  6604  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemres  6633  rdgtfr  6645  rdgruledefgg  6646  rdgon  6657  frecabex  6669  freccllem  6673  frecfcllem  6675  omcl  6734  oeicl  6735  erth  6853  th3qlem1  6911  mapex  6928  pmvalg  6933  mapfoss  6947  mapsnconst  6976  ixpexgg  7004  fundmen  7094  cnvct  7097  mapsnend  7099  snfig  7103  unen  7105  xpdom2  7129  mapxpen  7148  phplem2  7154  findcard2  7193  findcard2s  7194  infnfi  7199  relcnvfi  7255  sbthlemi8  7281  sbthlemi10  7283  fival  7304  fiss  7311  inl11  7405  casef  7428  caseinj  7429  caseinl  7431  caseinr  7432  djudom  7433  difinfsn  7440  djuinj  7446  0ct  7447  ctmlemr  7448  ctssdccl  7451  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  djuassen  7573  xpdjuen  7574  djudoml  7575  djudomr  7576  cc2lem  7632  ltnnnq  7790  nnnq0lem1  7813  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  suplocexprlem2b  8081  prsrlem1  8109  gt0srpr  8115  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsrlembound  8161  mulcnsr  8202  mulcnsrec  8210  addvalex  8211  pitoregt0  8216  axmulass  8240  axdistr  8241  recriota  8257  mulrid  8323  axmulgt0  8397  cnegexlem2  8502  cnegex  8504  gt0ne0d  8840  recexre  8906  msqge0  8944  mulge0  8947  aptap  8978  recgt0  9180  recreclt  9230  cju  9291  nnge1  9327  nnnlt1  9330  nn0nlt0  9589  nnnle0  9693  elz2  9716  nnm1ge0  9732  recnz  9739  zneo  9747  uz3m2nn  9973  eluz2b2  10003  nn01to3  10017  mnflt  10185  xnn0dcle  10204  xltadd1  10278  lincmb01cmp  10405  iccf1o  10407  fz1n  10448  fseq1p1m1  10501  fznn0  10520  fzctr  10540  4fvwrd4  10547  fzo0n  10575  elfzonlteqm1  10628  divfl0  10731  modqelico  10771  zmodfz  10783  modqid  10786  modqmuladdim  10804  m1modge3gt1  10808  addmodid  10809  frec2uzf1od  10843  frecfzennn  10863  frecfzen2  10864  fzfig  10867  ser0  10970  ser3le  10974  expgt1  11014  expubnd  11033  iexpcyc  11081  binom2sub  11090  binom3  11094  zesq  11096  bernneq  11098  bernneq2  11099  expnbnd  11101  expnlbnd2  11103  facdiv  11176  faclbnd2  11180  faclbnd3  11181  bcval4  11190  hashinfom  11217  hashennn  11219  fihashf1rn  11227  isfinite4im  11231  hashfz  11262  ssenneg  11280  hashf1lem1  11285  hashf1lem2  11286  iswrd  11306  iswrdiz  11311  wrdexg  11315  wrdexb  11316  wrdfin  11323  wrdnval  11335  wrdred1hash  11348  ccatsymb  11370  ccatalpha  11381  s111  11399  fzowrddc  11419  swrdlen  11424  swrdwrdsymbg  11436  pfxval  11446  pfx0g  11448  fnpfx  11449  pfxlen  11457  cats1un  11493  swrdccat  11507  crre  11622  crim  11623  remim  11625  mulreap  11629  cjreb  11631  recj  11632  reneg  11633  readd  11634  remullem  11636  imcj  11640  imneg  11641  imadd  11642  cjadd  11649  cjneg  11655  imval2  11659  cjreim  11669  cnrecnv  11676  uzin2  11753  absval  11767  rennim  11768  resqrexlemcalc3  11782  resqrexlemnm  11784  resqrexlemcvg  11785  resqrexlemgt0  11786  resqrexlemga  11789  absreimsq  11833  absreim  11834  amgm2  11884  climconst2  12057  climshft  12070  climshft2  12072  reccn2ap  12079  climge0  12091  sumsnf  12176  sumnul  12191  isumcl  12192  fsum2dlemstep  12201  fisumcom2  12205  fsumabs  12232  fsumiun  12244  binom  12251  bcxmas  12256  arisum  12265  expcnvap0  12269  explecnv  12272  geosergap  12273  geolim  12278  geolim2  12279  geo2sum  12281  geo2lim  12283  cvgratnnlemrate  12297  cvgratz  12299  mertenslemi1  12302  prodf1  12309  prodeq2w  12323  fprodntrivap  12351  prodsnf  12359  fprod2dlemstep  12389  fprodcom2fi  12393  efcllemp  12425  ege2le3  12438  eftlub  12457  efgt1  12464  tanval2ap  12480  tanval3ap  12481  resinval  12482  recosval  12483  efi4p  12484  resin4p  12485  recos4p  12486  resincl  12487  recoscl  12488  efmival  12500  efeul  12501  sinadd  12503  cosadd  12504  tanaddap  12506  sinmul  12511  cos2tsin  12518  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  sin01gt0  12529  cos01gt0  12530  absef  12537  absefib  12538  efieq1re  12539  demoivreALT  12541  eirraplem  12544  3dvds  12631  odd2np1  12640  oddm1even  12642  oddp1even  12643  oexpneg  12644  opoe  12662  omoe  12663  nn0o1gt2  12672  nn0o  12674  bitsdc  12714  bitsfzolem  12721  bitsfzo  12722  bitsinv1lem  12728  bitsinv1  12729  nninfctlemfo  12817  algcvg  12826  algcvgblem  12827  1nprm  12892  1idssfct  12893  oddprmge3  12913  divgcdodd  12921  pw2dvdslemn  12943  pw2dvds  12944  oddpwdclemodd  12950  oddpwdc  12952  phicl2  12992  phibndlem  12994  phibnd  12995  hashdvds  12999  crth  13002  phimullem  13003  eulerthlemfi  13006  eulerthlemrprm  13007  eulerthlema  13008  hashgcdeq  13018  phisum  13019  oddprm  13038  prm23ge5  13043  pythagtriplem1  13044  pythagtriplem4  13047  pythagtriplem12  13054  pythagtriplem14  13056  pczpre  13076  pcadd  13119  pcmpt  13122  pockthlem  13135  pockthi  13137  infpnlem2  13139  gzreim  13158  4sqlem11  13180  4sqlem12  13181  4sqlem13m  13182  4sqlem17  13186  2expltfac  13218  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemefi  13237  ballotfilemodife  13240  ballotfilem4  13241  evenennn  13284  ennnfonelemjn  13293  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemnn0  13313  exmidunben  13317  ctinfomlemom  13318  ssnnctlemct  13337  nninfdc  13344  slotex  13379  setscom  13392  strslfv3  13398  setsslid  13403  bassetsnn  13409  basmex  13412  basmexd  13413  relelbasov  13416  ressbas2d  13422  ressbasid  13424  strressid  13425  ressval3d  13426  2strbas1g  13477  2strop1g  13478  rngbaseg  13490  rngplusgg  13491  rngmulrg  13492  srngbased  13501  srngplusgd  13502  srngmulrd  13503  srnginvld  13504  lmodbased  13519  lmodplusgd  13520  lmodscad  13521  lmodvscad  13522  ipsbased  13531  ipsaddgd  13532  ipsmulrd  13533  ipsscad  13534  ipsvscad  13535  ipsipd  13536  topgrpbasd  13551  topgrpplusgd  13552  topgrptsetd  13553  tgvalex  13617  imasex  13626  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  imasaddfn  13638  imasaddval  13639  imasaddf  13640  imasmulfn  13641  imasmulval  13642  imasmulf  13643  qusval  13644  qusex  13646  qusaddvallemg  13654  qusaddflemg  13655  qusaddval  13656  qusaddf  13657  qusmulval  13658  qusmulf  13659  xpsfval  13669  plusffvalg  13682  grpidvalg  13693  gzsumvalx  13709  gzsumfzval  13711  gzsumress  13712  gzsum0  13713  gzsumval2  13714  issubmnd  13755  ress0g  13756  ismhm  13768  mhmex  13769  issubm  13779  0mhm  13793  grppropstrg  13824  grpinvfvalg  13847  grpinvval  13848  grpinvfng  13849  grpsubfvalg  13850  grpsubval  13851  grpressid  13866  grplactfval  13906  qusgrp2  13916  mulgfvalg  13924  mulgex  13926  mulgnngzsum  13930  issubg  13976  subgex  13979  subgmulg  13991  issubg2m  13992  releqgg  14023  eqgex  14024  eqgfval  14025  eqgen  14030  isghm  14046  ablressid  14139  gsumsncmn  14156  gsump1  14157  gsummptfidmadd  14161  prdsex  14172  prdsval  14173  prdsbaslemss  14174  prdsbas  14176  prdsplusg  14177  prdsmulr  14178  xpsval  14201  pwsbas  14205  pwselbasb  14206  pwssnf1o  14211  mgptopng  14228  rngressid  14253  qusrng  14257  dfur2g  14266  ringidss  14334  ring1  14364  ringressid  14368  qusring2  14371  opprringb  14386  dvdsrvald  14400  dvdsrex  14405  unitgrp  14423  unitabl  14424  invrfvald  14429  unitlinv  14433  unitrinv  14434  dvrfvald  14440  rdivmuldivd  14451  invrpropdg  14456  rhmunitinv  14485  isnzr2  14491  issubrng  14507  issubrg  14529  subrgugrp  14548  subrgpropd  14561  rrgmex  14569  aprval  14591  aprprop  14601  islmod  14627  scaffvalg  14643  lssex  14691  lssmex  14692  lsssetm  14693  islssmg  14695  islss3  14716  lspfval  14725  lspval  14727  lspcl  14728  lspex  14732  sralemg  14775  srascag  14779  sravscag  14780  sraipg  14781  sraex  14783  rlmsubg  14795  rlmvnegg  14802  ixpsnbasval  14803  lidlvalg  14808  rspvalg  14809  lidlex  14810  rspex  14811  lidlmex  14812  lidlss  14813  lidlrsppropdg  14832  2idlmex  14838  qusrhm  14865  gsumfsum  14923  znlidl  14969  zncrng2  14970  znval  14971  znle  14972  znbaslemnn  14974  znbas  14979  znzrh2  14981  znzrhval  14982  znzrhfo  14983  zndvds  14984  znfi  14990  znhash  14991  znidom  14992  znidomb  14993  aspval  15015  aspsubrg  15018  asclfval  15021  psrval  15050  psrbasg  15065  psrelbas  15066  psrplusgg  15069  psraddcl  15071  psr0cl  15072  psrnegcl  15074  psr1clfi  15079  mplvalcoe  15081  mplplusgg  15094  toponsspwpwg  15123  topgele  15130  istps  15133  topontopn  15138  tgclb  15166  lmfval  15294  lmres  15349  ispsmet  15424  psmetge0  15432  ismet  15445  isxmet  15446  xmetge0  15466  isxms2  15553  comet  15600  bdxmet  15602  cnmetdval  15630  cnbl0  15635  cnblcld  15636  reopnap  15647  tgioo  15655  cncfcncntop  15694  cncfmpt2fcntop  15700  maxcncf  15716  mincncf  15717  hovergt0  15751  limcimolemlt  15765  cnplimcim  15768  cnplimclemr  15770  limccnpcntop  15776  limccnp2lem  15777  limccnp2cntop  15778  dvfvalap  15782  dvbss  15786  dvcnp2cntop  15800  dvcn  15801  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvrecap  15814  dvmptfsum  15826  dveflem  15827  plyval  15833  plycolemc  15859  dvply2  15868  reeff1olem  15872  pilem3  15884  ef2kpi  15907  efper  15908  sinperlem  15909  efimpi  15920  ptolemy  15925  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  cosq14gt0  15933  tangtx  15939  sinkpi  15948  coskpi  15949  cosordlem  15950  rplogcl  15980  logge0  15981  logdivlti  15982  logbleb  16063  logblt  16064  binom4  16081  log2tlbndlog2  16082  log2ublem2  16084  log2ublog2  16086  birthdaylem2  16088  wilthlem1  16094  1sgmprm  16108  1sgm2ppw  16109  mersenne  16111  perfect1  16112  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgsval2lem  16129  lgsval4a  16141  lgsneg  16143  lgsdilem  16146  lgsdirprm  16153  lgsdirnn0  16166  gausslemma2dlem0i  16176  gausslemma2dlem6  16186  gausslemma2dlem7  16187  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlemofi  16195  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem2  16201  lgsquad2  16202  m1lgs  16204  2lgs  16223  2lgsoddprmlem2  16225  2lgsoddprm  16232  2sqlem2  16234  vtxvalg  16257  vtxex  16259  struct2slots2dom  16279  structvtxval  16280  structiedg0val  16281  structgrssvtx  16283  structgrssiedg  16284  edgstruct  16305  vdegp1bid  16556  wlkv0  16610  upgr2wlkdc  16618  clwwlkex  16639  clwwlkccatlem  16641  eupthfi  16692  trlsegvdeglem6  16706  konigsberglem1  16729  konigsberglem5  16733  depindlem1  16747  pwf1oexmid  17029  nnnninfex  17065  repiecege0  17076  isomninnlem  17079  iswomninnlem  17099  ismkvnnlem  17102