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  4094  unipw  4219  opeluu  4452  uniexb  4475  unon  4512  onintrab2im  4519  xpexg  4742  resiexg  4954  imaexg  4984  exse2  5004  soirri  5025  djudisj  5058  elxp5  5119  cnvexg  5168  cnviinm  5172  coexg  5175  funssres  5260  f1oabexg  5475  sefvex  5538  ssimaex  5579  mptfvex  5603  f1ompt  5669  fmptcof  5685  resfunexg  5739  mptexg  5743  funfvima3  5752  ovid  5993  ov  5996  ofres  6099  cofunexg  6112  opabex3d  6124  opabex3  6125  oprabexd  6130  1stcof  6166  2ndcof  6167  mpoexxg  6213  cnvf1o  6228  f2ndf  6229  algrflemg  6233  tposexg  6261  tfrlemisucaccv  6328  tfrlemibxssdm  6330  tfrlemibfn  6331  tfrlemi14d  6336  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemres  6352  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemres  6365  rdgtfr  6377  rdgruledefgg  6378  rdgon  6389  frecabex  6401  freccllem  6405  frecfcllem  6407  omcl  6464  oeicl  6465  erth  6581  th3qlem1  6639  mapex  6656  pmvalg  6661  mapsnconst  6696  ixpexgg  6724  fundmen  6808  cnvct  6811  snfig  6816  unen  6818  xpdom2  6833  mapxpen  6850  phplem2  6855  findcard2  6891  findcard2s  6892  infnfi  6897  relcnvfi  6942  sbthlemi8  6965  sbthlemi10  6967  fival  6971  fiss  6978  inl11  7066  casef  7089  caseinj  7090  caseinl  7092  caseinr  7093  djudom  7094  difinfsn  7101  djuinj  7107  0ct  7108  ctmlemr  7109  ctssdccl  7112  enomnilem  7138  enmkvlem  7161  enwomnilem  7169  djuassen  7218  xpdjuen  7219  djudoml  7220  djudomr  7221  cc2lem  7267  ltnnnq  7424  nnnq0lem1  7447  addnqprlemfl  7560  addnqprlemfu  7561  mulnqprlemfl  7576  mulnqprlemfu  7577  suplocexprlem2b  7715  prsrlem1  7743  gt0srpr  7749  caucvgsrlemcl  7790  caucvgsrlemfv  7792  caucvgsrlembound  7795  mulcnsr  7836  mulcnsrec  7844  addvalex  7845  pitoregt0  7850  axmulass  7874  axdistr  7875  recriota  7891  mulrid  7956  axmulgt0  8031  cnegexlem2  8135  cnegex  8137  gt0ne0d  8471  recexre  8537  msqge0  8575  mulge0  8578  aptap  8609  recgt0  8809  recreclt  8859  cju  8920  nnge1  8944  nnnlt1  8947  nn0nlt0  9204  elz2  9326  nnm1ge0  9341  recnz  9348  zneo  9356  uz3m2nn  9575  eluz2b2  9605  nn01to3  9619  mnflt  9785  xnn0dcle  9804  xltadd1  9878  lincmb01cmp  10005  iccf1o  10006  fz1n  10046  fseq1p1m1  10096  fznn0  10115  fzctr  10135  4fvwrd4  10142  elfzonlteqm1  10212  divfl0  10298  modqelico  10336  zmodfz  10348  modqid  10351  modqmuladdim  10369  m1modge3gt1  10373  addmodid  10374  frec2uzf1od  10408  frecfzennn  10428  frecfzen2  10429  fzfig  10432  ser0  10516  ser3le  10520  expgt1  10560  expubnd  10579  iexpcyc  10627  binom2sub  10636  binom3  10640  zesq  10641  bernneq  10643  bernneq2  10644  expnbnd  10646  expnlbnd2  10648  facdiv  10720  faclbnd2  10724  faclbnd3  10725  bcval4  10734  hashinfom  10760  hashennn  10762  fihashf1rn  10770  isfinite4im  10774  hashfz  10803  crre  10868  crim  10869  remim  10871  mulreap  10875  cjreb  10877  recj  10878  reneg  10879  readd  10880  remullem  10882  imcj  10886  imneg  10887  imadd  10888  cjadd  10895  cjneg  10901  imval2  10905  cjreim  10914  cnrecnv  10921  uzin2  10998  absval  11012  rennim  11013  resqrexlemcalc3  11027  resqrexlemnm  11029  resqrexlemcvg  11030  resqrexlemgt0  11031  resqrexlemga  11034  absreimsq  11078  absreim  11079  amgm2  11129  climconst2  11301  climshft  11314  climshft2  11316  reccn2ap  11323  climge0  11335  sumsnf  11419  sumnul  11434  isumcl  11435  fsum2dlemstep  11444  fisumcom2  11448  fsumabs  11475  fsumiun  11487  binom  11494  bcxmas  11499  arisum  11508  expcnvap0  11512  explecnv  11515  geosergap  11516  geolim  11521  geolim2  11522  geo2sum  11524  geo2lim  11526  cvgratnnlemrate  11540  cvgratz  11542  mertenslemi1  11545  prodf1  11552  prodeq2w  11566  fprodntrivap  11594  prodsnf  11602  fprod2dlemstep  11632  fprodcom2fi  11636  efcllemp  11668  ege2le3  11681  eftlub  11700  efgt1  11707  tanval2ap  11723  tanval3ap  11724  resinval  11725  recosval  11726  efi4p  11727  resin4p  11728  recos4p  11729  resincl  11730  recoscl  11731  efmival  11743  efeul  11744  sinadd  11746  cosadd  11747  tanaddap  11749  sinmul  11754  cos2tsin  11761  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  cos01gt0  11772  absef  11779  absefib  11780  efieq1re  11781  demoivreALT  11783  eirraplem  11786  odd2np1  11880  oddm1even  11882  oddp1even  11883  oexpneg  11884  opoe  11902  omoe  11903  nn0o1gt2  11912  nn0o  11914  algcvg  12050  algcvgblem  12051  1nprm  12116  1idssfct  12117  oddprmge3  12137  divgcdodd  12145  pw2dvdslemn  12167  pw2dvds  12168  oddpwdclemodd  12174  oddpwdc  12176  phicl2  12216  phibndlem  12218  phibnd  12219  hashdvds  12223  crth  12226  phimullem  12227  eulerthlemfi  12230  eulerthlemrprm  12231  eulerthlema  12232  hashgcdeq  12241  phisum  12242  oddprm  12261  prm23ge5  12266  pythagtriplem1  12267  pythagtriplem4  12270  pythagtriplem12  12277  pythagtriplem14  12279  pczpre  12299  pcadd  12341  pcmpt  12343  pockthlem  12356  pockthi  12358  infpnlem2  12360  gzreim  12379  evenennn  12396  ennnfonelemjn  12405  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemnn0  12425  exmidunben  12429  ctinfomlemom  12430  ssnnctlemct  12449  nninfdc  12456  slotex  12491  setscom  12504  setsslid  12515  basmex  12523  basmexd  12524  ressbas2d  12530  strressid  12532  ressval3d  12533  2strbas1g  12583  2strop1g  12584  rngbaseg  12596  rngplusgg  12597  rngmulrg  12598  srngbased  12607  srngplusgd  12608  srngmulrd  12609  srnginvld  12610  lmodbased  12625  lmodplusgd  12626  lmodscad  12627  lmodvscad  12628  ipsbased  12637  ipsaddgd  12638  ipsmulrd  12639  ipsscad  12640  ipsvscad  12641  ipsipd  12642  topgrpbasd  12657  topgrpplusgd  12658  topgrptsetd  12659  tgvalex  12717  prdsex  12723  imasex  12731  imasival  12732  imasbas  12733  imasplusg  12734  imasmulr  12735  imasaddfn  12743  imasaddval  12744  imasaddf  12745  imasmulfn  12746  imasmulval  12747  imasmulf  12748  qusval  12749  qusaddvallemg  12757  qusaddflemg  12758  qusaddval  12759  qusaddf  12760  qusmulval  12761  qusmulf  12762  xpsfval  12772  xpsval  12776  plusffvalg  12786  grpidvalg  12797  issubmnd  12848  ress0g  12849  ismhm  12858  issubm  12868  0mhm  12878  grppropstrg  12900  grpinvfvalg  12920  grpinvval  12921  grpinvfng  12922  grpsubfvalg  12923  grpsubval  12924  grpressid  12936  grplactfval  12976  mulgfvalg  12990  issubg  13038  subgex  13041  subgmulg  13053  issubg2m  13054  releqgg  13085  eqgfval  13086  eqgen  13091  mgptopng  13144  dfur2g  13150  ringidss  13217  ring1  13241  ringressid  13243  reldvdsrsrg  13266  dvdsrvald  13267  dvdsrex  13272  unitgrp  13290  unitabl  13291  invrfvald  13296  unitlinv  13300  unitrinv  13301  dvrfvald  13307  rdivmuldivd  13318  invrpropdg  13323  issubrg  13347  subrgugrp  13366  subrgpropd  13374  aprval  13377  islmod  13386  scaffvalg  13401  lsssetm  13449  islssm  13450  islss3  13471  toponsspwpwg  13561  topgele  13568  istps  13571  topontopn  13576  tgclb  13604  lmfval  13731  lmres  13787  ispsmet  13862  psmetge0  13870  ismet  13883  isxmet  13884  xmetge0  13904  isxms2  13991  comet  14038  bdxmet  14040  cnmetdval  14068  cnbl0  14073  cnblcld  14074  reopnap  14077  tgioo  14085  cncfcncntop  14119  cncfmpt2fcntop  14124  limcimolemlt  14172  cnplimcim  14175  cnplimclemr  14177  limccnpcntop  14183  limccnp2lem  14184  limccnp2cntop  14185  dvfvalap  14189  dvbss  14193  dvcnp2cntop  14202  dvcn  14203  dvaddxxbr  14204  dvmulxxbr  14205  dvcoapbr  14210  dvcjbr  14211  dvrecap  14216  dveflem  14226  reeff1olem  14231  pilem3  14243  ef2kpi  14266  efper  14267  sinperlem  14268  efimpi  14279  ptolemy  14284  sincosq2sgn  14287  sincosq3sgn  14288  sincosq4sgn  14289  sinq12gt0  14290  cosq14gt0  14292  tangtx  14298  sinkpi  14307  coskpi  14308  cosordlem  14309  rplogcl  14339  logge0  14340  logdivlti  14341  logbleb  14418  logblt  14419  binom4  14436  lgsval2lem  14450  lgsval4a  14462  lgsneg  14464  lgsdilem  14467  lgsdirprm  14474  lgsdirnn0  14487  lgseisenlem1  14489  lgseisenlem2  14490  m1lgs  14491  2lgsoddprmlem2  14493  2sqlem2  14501  pwf1oexmid  14788  isomninnlem  14817  iswomninnlem  14836  ismkvnnlem  14839