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  4183  unipw  4315  opeluu  4553  uniexb  4576  unon  4615  onintrab2im  4622  xpexg  4846  resiexg  5064  imaexg  5096  exse2  5117  soirri  5138  djudisj  5171  elxp5  5232  cnvexg  5281  cnviinm  5285  coexg  5288  funssres  5376  f1oabexg  5604  sefvex  5669  ssimaex  5716  mptfvex  5741  f1ompt  5806  fmptcof  5822  resfunexg  5883  mptexg  5889  funfvima3  5898  ovid  6148  ov  6151  ofres  6259  cofunexg  6280  opabex3d  6292  opabex3  6293  oprabexd  6298  1stcof  6335  2ndcof  6336  mpoexxg  6384  cnvf1o  6399  f2ndf  6400  algrflemg  6404  tposexg  6467  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemi14d  6542  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemres  6571  rdgtfr  6583  rdgruledefgg  6584  rdgon  6595  frecabex  6607  freccllem  6611  frecfcllem  6613  omcl  6672  oeicl  6673  erth  6791  th3qlem1  6849  mapex  6866  pmvalg  6871  mapsnconst  6906  ixpexgg  6934  fundmen  7024  cnvct  7027  snfig  7032  unen  7034  xpdom2  7058  mapxpen  7077  phplem2  7082  findcard2  7121  findcard2s  7122  infnfi  7127  relcnvfi  7183  sbthlemi8  7206  sbthlemi10  7208  fival  7212  fiss  7219  inl11  7307  casef  7330  caseinj  7331  caseinl  7333  caseinr  7334  djudom  7335  difinfsn  7342  djuinj  7348  0ct  7349  ctmlemr  7350  ctssdccl  7353  enomnilem  7380  enmkvlem  7403  enwomnilem  7411  djuassen  7475  xpdjuen  7476  djudoml  7477  djudomr  7478  cc2lem  7528  ltnnnq  7686  nnnq0lem1  7709  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprlemfl  7838  mulnqprlemfu  7839  suplocexprlem2b  7977  prsrlem1  8005  gt0srpr  8011  caucvgsrlemcl  8052  caucvgsrlemfv  8054  caucvgsrlembound  8057  mulcnsr  8098  mulcnsrec  8106  addvalex  8107  pitoregt0  8112  axmulass  8136  axdistr  8137  recriota  8153  mulrid  8219  axmulgt0  8293  cnegexlem2  8397  cnegex  8399  gt0ne0d  8734  recexre  8800  msqge0  8838  mulge0  8841  aptap  8872  recgt0  9072  recreclt  9122  cju  9183  nnge1  9208  nnnlt1  9211  nn0nlt0  9470  nnnle0  9572  elz2  9595  nnm1ge0  9610  recnz  9617  zneo  9625  uz3m2nn  9851  eluz2b2  9881  nn01to3  9895  mnflt  10062  xnn0dcle  10081  xltadd1  10155  lincmb01cmp  10282  iccf1o  10284  fz1n  10324  fseq1p1m1  10374  fznn0  10393  fzctr  10413  4fvwrd4  10420  fzo0n  10448  elfzonlteqm1  10501  divfl0  10602  modqelico  10642  zmodfz  10654  modqid  10657  modqmuladdim  10675  m1modge3gt1  10679  addmodid  10680  frec2uzf1od  10714  frecfzennn  10734  frecfzen2  10735  fzfig  10738  ser0  10841  ser3le  10845  expgt1  10885  expubnd  10904  iexpcyc  10952  binom2sub  10961  binom3  10965  zesq  10966  bernneq  10968  bernneq2  10969  expnbnd  10971  expnlbnd2  10973  facdiv  11046  faclbnd2  11050  faclbnd3  11051  bcval4  11060  hashinfom  11086  hashennn  11088  fihashf1rn  11096  isfinite4im  11100  hashfz  11131  iswrd  11164  iswrdiz  11169  wrdexg  11173  wrdexb  11174  wrdfin  11181  wrdnval  11193  wrdred1hash  11206  ccatsymb  11228  ccatalpha  11239  s111  11257  fzowrddc  11277  swrdlen  11282  swrdwrdsymbg  11294  pfxval  11304  pfx0g  11306  fnpfx  11307  pfxlen  11315  cats1un  11351  swrdccat  11365  crre  11480  crim  11481  remim  11483  mulreap  11487  cjreb  11489  recj  11490  reneg  11491  readd  11492  remullem  11494  imcj  11498  imneg  11499  imadd  11500  cjadd  11507  cjneg  11513  imval2  11517  cjreim  11526  cnrecnv  11533  uzin2  11610  absval  11624  rennim  11625  resqrexlemcalc3  11639  resqrexlemnm  11641  resqrexlemcvg  11642  resqrexlemgt0  11643  resqrexlemga  11646  absreimsq  11690  absreim  11691  amgm2  11741  climconst2  11914  climshft  11927  climshft2  11929  reccn2ap  11936  climge0  11948  sumsnf  12033  sumnul  12048  isumcl  12049  fsum2dlemstep  12058  fisumcom2  12062  fsumabs  12089  fsumiun  12101  binom  12108  bcxmas  12113  arisum  12122  expcnvap0  12126  explecnv  12129  geosergap  12130  geolim  12135  geolim2  12136  geo2sum  12138  geo2lim  12140  cvgratnnlemrate  12154  cvgratz  12156  mertenslemi1  12159  prodf1  12166  prodeq2w  12180  fprodntrivap  12208  prodsnf  12216  fprod2dlemstep  12246  fprodcom2fi  12250  efcllemp  12282  ege2le3  12295  eftlub  12314  efgt1  12321  tanval2ap  12337  tanval3ap  12338  resinval  12339  recosval  12340  efi4p  12341  resin4p  12342  recos4p  12343  resincl  12344  recoscl  12345  efmival  12357  efeul  12358  sinadd  12360  cosadd  12361  tanaddap  12363  sinmul  12368  cos2tsin  12375  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  sin01gt0  12386  cos01gt0  12387  absef  12394  absefib  12395  efieq1re  12396  demoivreALT  12398  eirraplem  12401  3dvds  12488  odd2np1  12497  oddm1even  12499  oddp1even  12500  oexpneg  12501  opoe  12519  omoe  12520  nn0o1gt2  12529  nn0o  12531  bitsdc  12571  bitsfzolem  12578  bitsfzo  12579  bitsinv1lem  12585  bitsinv1  12586  nninfctlemfo  12674  algcvg  12683  algcvgblem  12684  1nprm  12749  1idssfct  12750  oddprmge3  12770  divgcdodd  12778  pw2dvdslemn  12800  pw2dvds  12801  oddpwdclemodd  12807  oddpwdc  12809  phicl2  12849  phibndlem  12851  phibnd  12852  hashdvds  12856  crth  12859  phimullem  12860  eulerthlemfi  12863  eulerthlemrprm  12864  eulerthlema  12865  hashgcdeq  12875  phisum  12876  oddprm  12895  prm23ge5  12900  pythagtriplem1  12901  pythagtriplem4  12904  pythagtriplem12  12911  pythagtriplem14  12913  pczpre  12933  pcadd  12976  pcmpt  12979  pockthlem  12992  pockthi  12994  infpnlem2  12996  gzreim  13015  4sqlem11  13037  4sqlem12  13038  4sqlem13m  13039  4sqlem17  13043  2expltfac  13075  evenennn  13077  ennnfonelemjn  13086  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemnn0  13106  exmidunben  13110  ctinfomlemom  13111  ssnnctlemct  13130  nninfdc  13137  slotex  13172  setscom  13185  strslfv3  13191  setsslid  13196  bassetsnn  13202  basmex  13205  basmexd  13206  relelbasov  13208  ressbas2d  13214  ressbasid  13216  strressid  13217  ressval3d  13218  2strbas1g  13269  2strop1g  13270  rngbaseg  13282  rngplusgg  13283  rngmulrg  13284  srngbased  13293  srngplusgd  13294  srngmulrd  13295  srnginvld  13296  lmodbased  13311  lmodplusgd  13312  lmodscad  13313  lmodvscad  13314  ipsbased  13323  ipsaddgd  13324  ipsmulrd  13325  ipsscad  13326  ipsvscad  13327  ipsipd  13328  topgrpbasd  13343  topgrpplusgd  13344  topgrptsetd  13345  tgvalex  13409  prdsex  13415  prdsval  13419  prdsbaslemss  13420  prdsbas  13422  prdsplusg  13423  prdsmulr  13424  pwsbas  13438  pwselbasb  13439  pwssnf1o  13444  imasex  13451  imasival  13452  imasbas  13453  imasplusg  13454  imasmulr  13455  imasaddfn  13463  imasaddval  13464  imasaddf  13465  imasmulfn  13466  imasmulval  13467  imasmulf  13468  qusval  13469  qusex  13471  qusaddvallemg  13479  qusaddflemg  13480  qusaddval  13481  qusaddf  13482  qusmulval  13483  qusmulf  13484  xpsfval  13494  xpsval  13498  plusffvalg  13508  grpidvalg  13519  igsumvalx  13535  gsumfzval  13537  gsumress  13541  gsum0g  13542  gsumval2  13543  issubmnd  13588  ress0g  13589  ismhm  13607  mhmex  13608  issubm  13618  0mhm  13632  grppropstrg  13665  grpinvfvalg  13688  grpinvval  13689  grpinvfng  13690  grpsubfvalg  13691  grpsubval  13692  grpressid  13707  grplactfval  13747  qusgrp2  13763  mulgfvalg  13771  mulgex  13773  mulgnngsum  13777  issubg  13823  subgex  13826  subgmulg  13838  issubg2m  13839  releqgg  13870  eqgex  13871  eqgfval  13872  eqgen  13877  isghm  13893  ablressid  13985  mgptopng  14006  rngressid  14031  qusrng  14035  dfur2g  14039  ringidss  14106  ring1  14136  ringressid  14140  qusring2  14143  dvdsrvald  14171  dvdsrex  14176  unitgrp  14194  unitabl  14195  invrfvald  14200  unitlinv  14204  unitrinv  14205  dvrfvald  14211  rdivmuldivd  14222  invrpropdg  14227  rhmunitinv  14256  isnzr2  14262  issubrng  14277  issubrg  14299  subrgugrp  14318  subrgpropd  14331  rrgmex  14339  aprval  14361  islmod  14370  scaffvalg  14385  lssex  14433  lssmex  14434  lsssetm  14435  islssmg  14437  islss3  14458  lspfval  14467  lspval  14469  lspcl  14470  lspex  14474  sralemg  14517  srascag  14521  sravscag  14522  sraipg  14523  sraex  14525  rlmsubg  14537  rlmvnegg  14544  ixpsnbasval  14545  lidlvalg  14550  rspvalg  14551  lidlex  14552  rspex  14553  lidlmex  14554  lidlss  14555  lidlrsppropdg  14574  2idlmex  14580  qusrhm  14607  znlidl  14713  zncrng2  14714  znval  14715  znle  14716  znbaslemnn  14718  znbas  14723  znzrh2  14725  znzrhval  14726  znzrhfo  14727  zndvds  14728  znfi  14734  znhash  14735  znidom  14736  znidomb  14737  psrval  14745  psrbasg  14758  psrelbas  14759  psrplusgg  14762  psraddcl  14764  psr0cl  14765  psrnegcl  14767  psr1clfi  14772  mplvalcoe  14774  mplplusgg  14787  toponsspwpwg  14816  topgele  14823  istps  14826  topontopn  14831  tgclb  14859  lmfval  14987  lmres  15042  ispsmet  15117  psmetge0  15125  ismet  15138  isxmet  15139  xmetge0  15159  isxms2  15246  comet  15293  bdxmet  15295  cnmetdval  15323  cnbl0  15328  cnblcld  15329  reopnap  15340  tgioo  15348  cncfcncntop  15387  cncfmpt2fcntop  15393  maxcncf  15409  mincncf  15410  hovergt0  15444  limcimolemlt  15458  cnplimcim  15461  cnplimclemr  15463  limccnpcntop  15469  limccnp2lem  15470  limccnp2cntop  15471  dvfvalap  15475  dvbss  15479  dvcnp2cntop  15493  dvcn  15494  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  dvrecap  15507  dvmptfsum  15519  dveflem  15520  plyval  15526  plycolemc  15552  dvply2  15561  reeff1olem  15565  pilem3  15577  ef2kpi  15600  efper  15601  sinperlem  15602  efimpi  15613  ptolemy  15618  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  sinq12gt0  15624  cosq14gt0  15626  tangtx  15632  sinkpi  15641  coskpi  15642  cosordlem  15643  rplogcl  15673  logge0  15674  logdivlti  15675  logbleb  15755  logblt  15756  binom4  15773  wilthlem1  15777  1sgmprm  15791  1sgm2ppw  15792  mersenne  15794  perfect1  15795  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgsval2lem  15812  lgsval4a  15824  lgsneg  15826  lgsdilem  15829  lgsdirprm  15836  lgsdirnn0  15849  gausslemma2dlem0i  15859  gausslemma2dlem6  15869  gausslemma2dlem7  15870  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlemofi  15878  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem2  15884  lgsquad2  15885  m1lgs  15887  2lgs  15906  2lgsoddprmlem2  15908  2lgsoddprm  15915  2sqlem2  15917  vtxvalg  15940  vtxex  15942  struct2slots2dom  15962  structvtxval  15963  structiedg0val  15964  structgrssvtx  15966  structgrssiedg  15967  edgstruct  15988  vdegp1bid  16239  wlkv0  16293  upgr2wlkdc  16301  clwwlkex  16322  clwwlkccatlem  16324  eupthfi  16375  trlsegvdeglem6  16389  konigsberglem1  16412  konigsberglem5  16416  depindlem1  16430  pwf1oexmid  16704  nnnninfex  16731  repiecege0  16742  isomninnlem  16745  iswomninnlem  16765  ismkvnnlem  16768  gfsumsn  16797  gfsump1  16798