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  7406  casef  7429  caseinj  7430  caseinl  7432  caseinr  7433  djudom  7434  difinfsn  7441  djuinj  7447  0ct  7448  ctmlemr  7449  ctssdccl  7452  enomnilem  7479  enmkvlem  7502  enwomnilem  7510  djuassen  7574  xpdjuen  7575  djudoml  7576  djudomr  7577  cc2lem  7633  ltnnnq  7791  nnnq0lem1  7814  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemfl  7943  mulnqprlemfu  7944  suplocexprlem2b  8082  prsrlem1  8110  gt0srpr  8116  caucvgsrlemcl  8157  caucvgsrlemfv  8159  caucvgsrlembound  8162  mulcnsr  8203  mulcnsrec  8211  addvalex  8212  pitoregt0  8217  axmulass  8241  axdistr  8242  recriota  8258  mulrid  8324  axmulgt0  8398  cnegexlem2  8504  cnegex  8506  gt0ne0d  8842  recexre  8909  msqge0  8947  mulge0  8950  aptap  8981  recgt0  9183  recreclt  9233  cju  9294  nnge1  9330  nnnlt1  9333  nn0nlt0  9594  nnnle0  9698  elz2  9721  nnm1ge0  9737  recnz  9744  zneo  9752  uz3m2nn  9983  eluz2b2  10013  nn01to3  10027  mnflt  10196  xnn0dcle  10215  xltadd1  10289  lincmb01cmp  10416  iccf1o  10418  fz1n  10459  fseq1p1m1  10512  fznn0  10531  fzctr  10551  4fvwrd4  10558  fzo0n  10586  elfzonlteqm1  10639  divfl0  10746  modqelico  10786  zmodfz  10798  modqid  10801  modqmuladdim  10819  m1modge3gt1  10823  addmodid  10824  frec2uzf1od  10858  frecfzennn  10878  frecfzen2  10879  fzfig  10882  ser0  10985  ser3le  10989  expgt1  11029  expubnd  11048  iexpcyc  11096  binom2sub  11105  binom3  11109  zesq  11111  bernneq  11113  bernneq2  11114  expnbnd  11116  expnlbnd2  11118  facdiv  11192  faclbnd2  11196  faclbnd3  11197  bcval4  11206  hashinfom  11233  hashennn  11235  fihashf1rn  11243  isfinite4im  11247  hashfz  11278  ssenneg  11296  hashf1lem1  11301  hashf1lem2  11302  iswrd  11322  iswrdiz  11327  wrdexg  11331  wrdexb  11332  wrdfin  11339  wrdnval  11351  wrdred1hash  11364  ccatsymb  11386  ccatalpha  11397  s111  11415  fzowrddc  11435  swrdlen  11440  swrdwrdsymbg  11452  pfxval  11462  pfx0g  11464  fnpfx  11465  pfxlen  11473  cats1un  11509  swrdccat  11523  crre  11638  crim  11639  remim  11641  mulreap  11645  cjreb  11647  recj  11648  reneg  11649  readd  11650  remullem  11652  imcj  11656  imneg  11657  imadd  11658  cjadd  11665  cjneg  11671  imval2  11675  cjreim  11685  cnrecnv  11692  uzin2  11769  absval  11783  rennim  11784  resqrexlemcalc3  11798  resqrexlemnm  11800  resqrexlemcvg  11801  resqrexlemgt0  11802  resqrexlemga  11805  absreimsq  11849  absreim  11850  amgm2  11901  climconst2  12076  climshft  12089  climshft2  12091  reccn2ap  12098  climge0  12110  sumsnf  12195  sumnul  12210  isumcl  12211  fsum2dlemstep  12220  fisumcom2  12224  fsumabs  12251  fsumiun  12263  binom  12270  bcxmas  12275  arisum  12284  expcnvap0  12288  explecnv  12291  geosergap  12292  geolim  12297  geolim2  12298  geo2sum  12300  geo2lim  12302  cvgratnnlemrate  12316  cvgratz  12318  mertenslemi1  12321  prodf1  12328  prodeq2w  12342  fprodntrivap  12370  prodsnf  12378  fprod2dlemstep  12408  fprodcom2fi  12412  efcllemp  12444  ege2le3  12457  eftlub  12476  efgt1  12483  tanval2ap  12499  tanval3ap  12500  resinval  12501  recosval  12502  efi4p  12503  resin4p  12504  recos4p  12505  resincl  12506  recoscl  12507  efmival  12519  efeul  12520  sinadd  12522  cosadd  12523  tanaddap  12525  sinmul  12530  cos2tsin  12537  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  sin01gt0  12548  cos01gt0  12549  absef  12556  absefib  12557  efieq1re  12558  demoivreALT  12560  eirraplem  12563  3dvds  12650  odd2np1  12659  oddm1even  12661  oddp1even  12662  oexpneg  12663  opoe  12681  omoe  12682  nn0o1gt2  12691  nn0o  12693  bitsdc  12733  bitsfzolem  12740  bitsfzo  12741  bitsinv1lem  12747  bitsinv1  12748  nninfctlemfo  12836  algcvg  12845  algcvgblem  12846  1nprm  12911  1idssfct  12912  oddprmge3  12933  divgcdodd  12941  phicl2  13015  phibndlem  13017  phibnd  13018  hashdvds  13022  crth  13025  phimullem  13026  eulerthlemfi  13029  eulerthlemrprm  13030  eulerthlema  13031  hashgcdeq  13041  phisum  13042  oddprm  13061  prm23ge5  13066  pythagtriplem1  13067  pythagtriplem4  13070  pythagtriplem12  13077  pythagtriplem14  13079  pczpre  13099  pcadd  13142  pcmpt  13145  pockthlem  13158  pockthi  13160  infpnlem2  13162  gzreim  13181  4sqlem11  13203  4sqlem12  13204  4sqlem13m  13205  4sqlem17  13209  2expltfac  13242  prmlem0  13243  prmlem1  13245  prmlem2  13257  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemefi  13289  ballotfilemodife  13292  ballotfilem4  13293  evenennn  13336  ennnfonelemjn  13345  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemnn0  13365  exmidunben  13369  ctinfomlemom  13370  ssnnctlemct  13389  nninfdc  13396  slotex  13431  setscom  13444  strslfv3  13450  setsslid  13455  bassetsnn  13461  basmex  13464  basmexd  13465  relelbasov  13468  ressbas2d  13475  ressbasid  13477  strressid  13478  ressval3d  13479  2strbas1g  13530  2strop1g  13531  rngbaseg  13543  rngplusgg  13544  rngmulrg  13545  srngbased  13554  srngplusgd  13555  srngmulrd  13556  srnginvld  13557  lmodbased  13572  lmodplusgd  13573  lmodscad  13574  lmodvscad  13575  ipsbased  13584  ipsaddgd  13585  ipsmulrd  13586  ipsscad  13587  ipsvscad  13588  ipsipd  13589  topgrpbasd  13604  topgrpplusgd  13605  topgrptsetd  13606  tgvalex  13670  imasex  13679  imasival  13680  imasbas  13681  imasplusg  13682  imasmulr  13683  imasaddfn  13691  imasaddval  13692  imasaddf  13693  imasmulfn  13694  imasmulval  13695  imasmulf  13696  qusval  13697  qusex  13699  qusaddvallemg  13707  qusaddflemg  13708  qusaddval  13709  qusaddf  13710  qusmulval  13711  qusmulf  13712  xpsfval  13722  plusffvalg  13735  grpidvalg  13746  gzsumvalx  13762  gzsumfzval  13764  gzsumress  13765  gzsum0  13766  gzsumval2  13767  issubmnd  13808  ress0g  13809  ismhm  13821  mhmex  13822  issubm  13832  0mhm  13846  grppropstrg  13877  grpinvfvalg  13900  grpinvval  13901  grpinvfng  13902  grpsubfvalg  13903  grpsubval  13904  grpressid  13919  grplactfval  13959  qusgrp2  13969  mulgfvalg  13977  mulgex  13979  mulgnngzsum  13983  issubg  14029  subgex  14032  subgmulg  14044  issubg2m  14045  releqgg  14076  eqgex  14077  eqgfval  14078  eqgen  14083  isghm  14099  cntzex  14144  cntzfval  14146  cntzval  14147  cntz2ss  14162  ablressid  14223  gsumsncmn  14240  gsump1  14241  gsummptfidmadd  14245  prdsex  14256  prdsval  14257  prdsbaslemss  14258  prdsbas  14260  prdsplusg  14261  prdsmulr  14262  xpsval  14285  pwsbas  14289  pwselbasb  14290  pwssnf1o  14295  mgptopng  14312  rngressid  14337  qusrng  14341  dfur2g  14350  ringidss  14418  ring1  14448  ringressid  14452  qusring2  14455  opprringb  14470  dvdsrvald  14484  dvdsrex  14489  unitgrp  14507  unitabl  14508  invrfvald  14513  unitlinv  14517  unitrinv  14518  dvrfvald  14524  rdivmuldivd  14535  invrpropdg  14540  rhmunitinv  14569  isnzr2  14575  issubrng  14591  issubrg  14613  subrgugrp  14632  subrgpropd  14645  rrgmex  14653  aprval  14675  aprprop  14685  islmod  14711  scaffvalg  14727  lssex  14775  lssmex  14776  lsssetm  14777  islssmg  14779  islss3  14800  lspfval  14809  lspval  14811  lspcl  14812  lspex  14816  sralemg  14859  srascag  14863  sravscag  14864  sraipg  14865  sraex  14867  rlmsubg  14879  rlmvnegg  14886  ixpsnbasval  14887  lidlvalg  14892  rspvalg  14893  lidlex  14894  rspex  14895  lidlmex  14896  lidlss  14897  lidlrsppropdg  14916  2idlmex  14922  qusrhm  14949  gsumfsum  15007  znlidl  15053  zncrng2  15054  znval  15055  znle  15056  znbaslemnn  15058  znbas  15063  znzrh2  15065  znzrhval  15066  znzrhfo  15067  zndvds  15068  znfi  15074  znhash  15075  znidom  15076  znidomb  15077  aspval  15099  aspsubrg  15102  asclfval  15105  psrval  15134  psrbasg  15150  psrelbas  15151  psrplusgg  15154  psraddcl  15156  psrmulrg  15158  psrmulclfilem  15161  psr0cl  15163  psrnegcl  15165  psr1clfi  15170  mplvalcoe  15172  mplplusgg  15185  toponsspwpwg  15214  topgele  15221  istps  15224  topontopn  15229  tgclb  15257  lmfval  15385  lmres  15440  ispsmet  15515  psmetge0  15523  ismet  15536  isxmet  15537  xmetge0  15557  isxms2  15644  comet  15691  bdxmet  15693  cnmetdval  15721  cnbl0  15726  cnblcld  15727  reopnap  15738  tgioo  15746  cncfcncntop  15785  cncfmpt2fcntop  15791  maxcncf  15807  mincncf  15808  hovergt0  15842  limcimolemlt  15856  cnplimcim  15859  cnplimclemr  15861  limccnpcntop  15867  limccnp2lem  15868  limccnp2cntop  15869  dvfvalap  15873  dvbss  15877  dvcnp2cntop  15891  dvcn  15892  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvrecap  15905  dvmptfsum  15917  dveflem  15918  plyval  15924  plycolemc  15950  dvply2  15959  reeff1olem  15963  pilem3  15976  ef2kpi  15999  efper  16000  sinperlem  16001  efimpi  16012  ptolemy  16017  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  cosq14gt0  16025  tangtx  16031  sinkpi  16040  coskpi  16041  cosordlem  16042  rplogcl  16073  logge0  16074  logdivlti  16075  logbleb  16158  logblt  16159  binom4  16180  log2tlbndlog2  16181  log2ublem2  16183  log2ublog2  16185  birthdaylem2  16187  wilthlem1  16193  ppiqsval  16201  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  ppiqeq0  16241  1sgmprm  16249  1sgm2ppw  16250  ppiublem1  16252  ppiqub  16254  chtqleppi  16255  chtublem  16256  chtqub  16257  mersenne  16258  perfect1  16259  perfectlem1  16260  perfectlem2  16261  perfect  16262  bcmono  16265  bcmax  16266  bclbnd  16268  bpos1lem  16270  bpos1  16271  bposlem1  16272  bposlem2  16273  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgsval2lem  16295  lgsval4a  16307  lgsneg  16309  lgsdilem  16312  lgsdirprm  16319  lgsdirnn0  16332  gausslemma2dlem0i  16342  gausslemma2dlem6  16352  gausslemma2dlem7  16353  gausslemma2d  16354  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgsquadlemofi  16361  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem2  16367  lgsquad2  16368  m1lgs  16370  2lgs  16389  2lgsoddprmlem2  16391  2lgsoddprm  16398  2sqlem2  16400  vtxvalg  16423  vtxex  16425  struct2slots2dom  16445  structvtxval  16446  structiedg0val  16447  structgrssvtx  16449  structgrssiedg  16450  edgstruct  16471  vdegp1bid  16722  wlkv0  16776  upgr2wlkdc  16784  clwwlkex  16805  clwwlkccatlem  16807  eupthfi  16858  trlsegvdeglem6  16872  konigsberglem1  16895  konigsberglem5  16899  depindlem1  16913  pwf1oexmid  17195  nnnninfex  17231  repiecege0  17242  isomninnlem  17245  iswomninnlem  17266  ismkvnnlem  17269