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  4118  unipw  4246  opeluu  4481  uniexb  4504  unon  4543  onintrab2im  4550  xpexg  4773  resiexg  4987  imaexg  5019  exse2  5039  soirri  5060  djudisj  5093  elxp5  5154  cnvexg  5203  cnviinm  5207  coexg  5210  funssres  5296  f1oabexg  5512  sefvex  5575  ssimaex  5618  mptfvex  5643  f1ompt  5709  fmptcof  5725  resfunexg  5779  mptexg  5783  funfvima3  5792  ovid  6035  ov  6038  ofres  6145  cofunexg  6161  opabex3d  6173  opabex3  6174  oprabexd  6179  1stcof  6216  2ndcof  6217  mpoexxg  6263  cnvf1o  6278  f2ndf  6279  algrflemg  6283  tposexg  6311  tfrlemisucaccv  6378  tfrlemibxssdm  6380  tfrlemibfn  6381  tfrlemi14d  6386  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemres  6402  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemres  6415  rdgtfr  6427  rdgruledefgg  6428  rdgon  6439  frecabex  6451  freccllem  6455  frecfcllem  6457  omcl  6514  oeicl  6515  erth  6633  th3qlem1  6691  mapex  6708  pmvalg  6713  mapsnconst  6748  ixpexgg  6776  fundmen  6860  cnvct  6863  snfig  6868  unen  6870  xpdom2  6885  mapxpen  6904  phplem2  6909  findcard2  6945  findcard2s  6946  infnfi  6951  relcnvfi  7000  sbthlemi8  7023  sbthlemi10  7025  fival  7029  fiss  7036  inl11  7124  casef  7147  caseinj  7148  caseinl  7150  caseinr  7151  djudom  7152  difinfsn  7159  djuinj  7165  0ct  7166  ctmlemr  7167  ctssdccl  7170  enomnilem  7197  enmkvlem  7220  enwomnilem  7228  djuassen  7277  xpdjuen  7278  djudoml  7279  djudomr  7280  cc2lem  7326  ltnnnq  7483  nnnq0lem1  7506  addnqprlemfl  7619  addnqprlemfu  7620  mulnqprlemfl  7635  mulnqprlemfu  7636  suplocexprlem2b  7774  prsrlem1  7802  gt0srpr  7808  caucvgsrlemcl  7849  caucvgsrlemfv  7851  caucvgsrlembound  7854  mulcnsr  7895  mulcnsrec  7903  addvalex  7904  pitoregt0  7909  axmulass  7933  axdistr  7934  recriota  7950  mulrid  8016  axmulgt0  8091  cnegexlem2  8195  cnegex  8197  gt0ne0d  8531  recexre  8597  msqge0  8635  mulge0  8638  aptap  8669  recgt0  8869  recreclt  8919  cju  8980  nnge1  9005  nnnlt1  9008  nn0nlt0  9266  elz2  9388  nnm1ge0  9403  recnz  9410  zneo  9418  uz3m2nn  9638  eluz2b2  9668  nn01to3  9682  mnflt  9849  xnn0dcle  9868  xltadd1  9942  lincmb01cmp  10069  iccf1o  10070  fz1n  10110  fseq1p1m1  10160  fznn0  10179  fzctr  10199  4fvwrd4  10206  elfzonlteqm1  10277  divfl0  10365  modqelico  10405  zmodfz  10417  modqid  10420  modqmuladdim  10438  m1modge3gt1  10442  addmodid  10443  frec2uzf1od  10477  frecfzennn  10497  frecfzen2  10498  fzfig  10501  ser0  10604  ser3le  10608  expgt1  10648  expubnd  10667  iexpcyc  10715  binom2sub  10724  binom3  10728  zesq  10729  bernneq  10731  bernneq2  10732  expnbnd  10734  expnlbnd2  10736  facdiv  10809  faclbnd2  10813  faclbnd3  10814  bcval4  10823  hashinfom  10849  hashennn  10851  fihashf1rn  10859  isfinite4im  10863  hashfz  10892  iswrd  10916  iswrdiz  10921  wrdexg  10925  wrdexb  10926  wrdfin  10933  wrdnval  10944  wrdred1hash  10957  crre  11001  crim  11002  remim  11004  mulreap  11008  cjreb  11010  recj  11011  reneg  11012  readd  11013  remullem  11015  imcj  11019  imneg  11020  imadd  11021  cjadd  11028  cjneg  11034  imval2  11038  cjreim  11047  cnrecnv  11054  uzin2  11131  absval  11145  rennim  11146  resqrexlemcalc3  11160  resqrexlemnm  11162  resqrexlemcvg  11163  resqrexlemgt0  11164  resqrexlemga  11167  absreimsq  11211  absreim  11212  amgm2  11262  climconst2  11434  climshft  11447  climshft2  11449  reccn2ap  11456  climge0  11468  sumsnf  11552  sumnul  11567  isumcl  11568  fsum2dlemstep  11577  fisumcom2  11581  fsumabs  11608  fsumiun  11620  binom  11627  bcxmas  11632  arisum  11641  expcnvap0  11645  explecnv  11648  geosergap  11649  geolim  11654  geolim2  11655  geo2sum  11657  geo2lim  11659  cvgratnnlemrate  11673  cvgratz  11675  mertenslemi1  11678  prodf1  11685  prodeq2w  11699  fprodntrivap  11727  prodsnf  11735  fprod2dlemstep  11765  fprodcom2fi  11769  efcllemp  11801  ege2le3  11814  eftlub  11833  efgt1  11840  tanval2ap  11856  tanval3ap  11857  resinval  11858  recosval  11859  efi4p  11860  resin4p  11861  recos4p  11862  resincl  11863  recoscl  11864  efmival  11876  efeul  11877  sinadd  11879  cosadd  11880  tanaddap  11882  sinmul  11887  cos2tsin  11894  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  sin01gt0  11905  cos01gt0  11906  absef  11913  absefib  11914  efieq1re  11915  demoivreALT  11917  eirraplem  11920  odd2np1  12014  oddm1even  12016  oddp1even  12017  oexpneg  12018  opoe  12036  omoe  12037  nn0o1gt2  12046  nn0o  12048  nninfctlemfo  12177  algcvg  12186  algcvgblem  12187  1nprm  12252  1idssfct  12253  oddprmge3  12273  divgcdodd  12281  pw2dvdslemn  12303  pw2dvds  12304  oddpwdclemodd  12310  oddpwdc  12312  phicl2  12352  phibndlem  12354  phibnd  12355  hashdvds  12359  crth  12362  phimullem  12363  eulerthlemfi  12366  eulerthlemrprm  12367  eulerthlema  12368  hashgcdeq  12377  phisum  12378  oddprm  12397  prm23ge5  12402  pythagtriplem1  12403  pythagtriplem4  12406  pythagtriplem12  12413  pythagtriplem14  12415  pczpre  12435  pcadd  12478  pcmpt  12481  pockthlem  12494  pockthi  12496  infpnlem2  12498  gzreim  12517  4sqlem11  12539  4sqlem12  12540  4sqlem13m  12541  4sqlem17  12545  evenennn  12550  ennnfonelemjn  12559  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemnn0  12579  exmidunben  12583  ctinfomlemom  12584  ssnnctlemct  12603  nninfdc  12610  slotex  12645  setscom  12658  setsslid  12669  basmex  12677  basmexd  12678  relelbasov  12680  ressbas2d  12686  ressbasid  12688  strressid  12689  ressval3d  12690  2strbas1g  12740  2strop1g  12741  rngbaseg  12753  rngplusgg  12754  rngmulrg  12755  srngbased  12764  srngplusgd  12765  srngmulrd  12766  srnginvld  12767  lmodbased  12782  lmodplusgd  12783  lmodscad  12784  lmodvscad  12785  ipsbased  12794  ipsaddgd  12795  ipsmulrd  12796  ipsscad  12797  ipsvscad  12798  ipsipd  12799  topgrpbasd  12814  topgrpplusgd  12815  topgrptsetd  12816  tgvalex  12874  prdsex  12880  imasex  12888  imasival  12889  imasbas  12890  imasplusg  12891  imasmulr  12892  imasaddfn  12900  imasaddval  12901  imasaddf  12902  imasmulfn  12903  imasmulval  12904  imasmulf  12905  qusval  12906  qusex  12908  qusaddvallemg  12916  qusaddflemg  12917  qusaddval  12918  qusaddf  12919  qusmulval  12920  qusmulf  12921  xpsfval  12931  xpsval  12935  plusffvalg  12945  grpidvalg  12956  igsumvalx  12972  gsumfzval  12974  gsumress  12978  gsum0g  12979  gsumval2  12980  issubmnd  13023  ress0g  13024  ismhm  13033  mhmex  13034  issubm  13044  0mhm  13058  grppropstrg  13091  grpinvfvalg  13114  grpinvval  13115  grpinvfng  13116  grpsubfvalg  13117  grpsubval  13118  grpressid  13133  grplactfval  13173  qusgrp2  13183  mulgfvalg  13191  mulgex  13193  mulgnngsum  13197  issubg  13243  subgex  13246  subgmulg  13258  issubg2m  13259  releqgg  13290  eqgex  13291  eqgfval  13292  eqgen  13297  isghm  13313  ablressid  13405  mgptopng  13425  rngressid  13450  qusrng  13454  dfur2g  13458  ringidss  13525  ring1  13555  ringressid  13559  qusring2  13562  reldvdsrsrg  13588  dvdsrvald  13589  dvdsrex  13594  unitgrp  13612  unitabl  13613  invrfvald  13618  unitlinv  13622  unitrinv  13623  dvrfvald  13629  rdivmuldivd  13640  invrpropdg  13645  rhmunitinv  13674  isnzr2  13680  issubrng  13695  issubrg  13717  subrgugrp  13736  subrgpropd  13749  rrgmex  13757  aprval  13778  islmod  13787  scaffvalg  13802  lssex  13850  lssmex  13851  lsssetm  13852  islssmg  13854  islss3  13875  lspfval  13884  lspval  13886  lspcl  13887  lspex  13891  sralemg  13934  srascag  13938  sravscag  13939  sraipg  13940  sraex  13942  rlmsubg  13954  rlmvnegg  13961  ixpsnbasval  13962  lidlvalg  13967  rspvalg  13968  lidlex  13969  rspex  13970  lidlmex  13971  lidlss  13972  lidlrsppropdg  13991  2idlmex  13997  qusrhm  14024  znlidl  14122  zncrng2  14123  znval  14124  znle  14125  znbaslemnn  14127  znbas  14132  znzrh2  14134  znzrhval  14135  znzrhfo  14136  zndvds  14137  znfi  14143  znhash  14144  znidom  14145  znidomb  14146  psrval  14152  psrbasg  14159  psrelbas  14160  psrplusgg  14162  psraddcl  14164  toponsspwpwg  14190  topgele  14197  istps  14200  topontopn  14205  tgclb  14233  lmfval  14360  lmres  14416  ispsmet  14491  psmetge0  14499  ismet  14512  isxmet  14513  xmetge0  14533  isxms2  14620  comet  14667  bdxmet  14669  cnmetdval  14697  cnbl0  14702  cnblcld  14703  reopnap  14706  tgioo  14714  cncfcncntop  14748  cncfmpt2fcntop  14753  maxcncf  14769  mincncf  14770  hovergt0  14804  limcimolemlt  14818  cnplimcim  14821  cnplimclemr  14823  limccnpcntop  14829  limccnp2lem  14830  limccnp2cntop  14831  dvfvalap  14835  dvbss  14839  dvcnp2cntop  14848  dvcn  14849  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvrecap  14862  dveflem  14872  plyval  14878  reeff1olem  14906  pilem3  14918  ef2kpi  14941  efper  14942  sinperlem  14943  efimpi  14954  ptolemy  14959  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  cosq14gt0  14967  tangtx  14973  sinkpi  14982  coskpi  14983  cosordlem  14984  rplogcl  15014  logge0  15015  logdivlti  15016  logbleb  15093  logblt  15094  binom4  15111  wilthlem1  15112  lgsval2lem  15126  lgsval4a  15138  lgsneg  15140  lgsdilem  15143  lgsdirprm  15150  lgsdirnn0  15163  gausslemma2dlem0i  15173  gausslemma2dlem6  15183  gausslemma2dlem7  15184  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem2  15194  2sqlem2  15202  pwf1oexmid  15490  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542