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  4204  unipw  4338  opeluu  4576  uniexb  4599  unon  4638  onintrab2im  4645  xpexg  4869  resiexg  5088  imaexg  5120  exse2  5141  soirri  5162  djudisj  5195  elxp5  5256  cnvexg  5305  cnviinm  5309  coexg  5312  funssres  5400  f1oabexg  5631  sefvex  5696  ssimaex  5743  mptfvex  5768  f1ompt  5833  fmptcof  5849  resfunexg  5910  mptexg  5916  funfvima3  5925  ovid  6178  ov  6181  ofres  6290  cofunexg  6311  opabex3d  6323  opabex3  6324  oprabexd  6333  1stcof  6370  2ndcof  6371  mpoexxg  6419  cnvf1o  6434  f2ndf  6435  algrflemg  6439  tposexg  6502  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemi14d  6577  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemres  6606  rdgtfr  6618  rdgruledefgg  6619  rdgon  6630  frecabex  6642  freccllem  6646  frecfcllem  6648  omcl  6707  oeicl  6708  erth  6826  th3qlem1  6884  mapex  6901  pmvalg  6906  mapsnconst  6942  ixpexgg  6970  fundmen  7060  cnvct  7063  mapsnend  7065  snfig  7069  unen  7071  xpdom2  7095  mapxpen  7114  phplem2  7120  findcard2  7159  findcard2s  7160  infnfi  7165  relcnvfi  7221  sbthlemi8  7247  sbthlemi10  7249  fival  7270  fiss  7277  inl11  7369  casef  7392  caseinj  7393  caseinl  7395  caseinr  7396  djudom  7397  difinfsn  7404  djuinj  7410  0ct  7411  ctmlemr  7412  ctssdccl  7415  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  djuassen  7537  xpdjuen  7538  djudoml  7539  djudomr  7540  cc2lem  7596  ltnnnq  7754  nnnq0lem1  7777  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemfl  7906  mulnqprlemfu  7907  suplocexprlem2b  8045  prsrlem1  8073  gt0srpr  8079  caucvgsrlemcl  8120  caucvgsrlemfv  8122  caucvgsrlembound  8125  mulcnsr  8166  mulcnsrec  8174  addvalex  8175  pitoregt0  8180  axmulass  8204  axdistr  8205  recriota  8221  mulrid  8287  axmulgt0  8361  cnegexlem2  8465  cnegex  8467  gt0ne0d  8803  recexre  8869  msqge0  8907  mulge0  8910  aptap  8941  recgt0  9141  recreclt  9191  cju  9252  nnge1  9277  nnnlt1  9280  nn0nlt0  9539  nnnle0  9643  elz2  9666  nnm1ge0  9682  recnz  9689  zneo  9697  uz3m2nn  9923  eluz2b2  9953  nn01to3  9967  mnflt  10135  xnn0dcle  10154  xltadd1  10228  lincmb01cmp  10355  iccf1o  10357  fz1n  10398  fseq1p1m1  10450  fznn0  10469  fzctr  10489  4fvwrd4  10496  fzo0n  10524  elfzonlteqm1  10577  divfl0  10680  modqelico  10720  zmodfz  10732  modqid  10735  modqmuladdim  10753  m1modge3gt1  10757  addmodid  10758  frec2uzf1od  10792  frecfzennn  10812  frecfzen2  10813  fzfig  10816  ser0  10919  ser3le  10923  expgt1  10963  expubnd  10982  iexpcyc  11030  binom2sub  11039  binom3  11043  zesq  11045  bernneq  11047  bernneq2  11048  expnbnd  11050  expnlbnd2  11052  facdiv  11125  faclbnd2  11129  faclbnd3  11130  bcval4  11139  hashinfom  11166  hashennn  11168  fihashf1rn  11176  isfinite4im  11180  hashfz  11211  ssenneg  11229  iswrd  11251  iswrdiz  11256  wrdexg  11260  wrdexb  11261  wrdfin  11268  wrdnval  11280  wrdred1hash  11293  ccatsymb  11315  ccatalpha  11326  s111  11344  fzowrddc  11364  swrdlen  11369  swrdwrdsymbg  11381  pfxval  11391  pfx0g  11393  fnpfx  11394  pfxlen  11402  cats1un  11438  swrdccat  11452  crre  11567  crim  11568  remim  11570  mulreap  11574  cjreb  11576  recj  11577  reneg  11578  readd  11579  remullem  11581  imcj  11585  imneg  11586  imadd  11587  cjadd  11594  cjneg  11600  imval2  11604  cjreim  11613  cnrecnv  11620  uzin2  11697  absval  11711  rennim  11712  resqrexlemcalc3  11726  resqrexlemnm  11728  resqrexlemcvg  11729  resqrexlemgt0  11730  resqrexlemga  11733  absreimsq  11777  absreim  11778  amgm2  11828  climconst2  12001  climshft  12014  climshft2  12016  reccn2ap  12023  climge0  12035  sumsnf  12120  sumnul  12135  isumcl  12136  fsum2dlemstep  12145  fisumcom2  12149  fsumabs  12176  fsumiun  12188  binom  12195  bcxmas  12200  arisum  12209  expcnvap0  12213  explecnv  12216  geosergap  12217  geolim  12222  geolim2  12223  geo2sum  12225  geo2lim  12227  cvgratnnlemrate  12241  cvgratz  12243  mertenslemi1  12246  prodf1  12253  prodeq2w  12267  fprodntrivap  12295  prodsnf  12303  fprod2dlemstep  12333  fprodcom2fi  12337  efcllemp  12369  ege2le3  12382  eftlub  12401  efgt1  12408  tanval2ap  12424  tanval3ap  12425  resinval  12426  recosval  12427  efi4p  12428  resin4p  12429  recos4p  12430  resincl  12431  recoscl  12432  efmival  12444  efeul  12445  sinadd  12447  cosadd  12448  tanaddap  12450  sinmul  12455  cos2tsin  12462  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  cos01gt0  12474  absef  12481  absefib  12482  efieq1re  12483  demoivreALT  12485  eirraplem  12488  3dvds  12575  odd2np1  12584  oddm1even  12586  oddp1even  12587  oexpneg  12588  opoe  12606  omoe  12607  nn0o1gt2  12616  nn0o  12618  bitsdc  12658  bitsfzolem  12665  bitsfzo  12666  bitsinv1lem  12672  bitsinv1  12673  nninfctlemfo  12761  algcvg  12770  algcvgblem  12771  1nprm  12836  1idssfct  12837  oddprmge3  12857  divgcdodd  12865  pw2dvdslemn  12887  pw2dvds  12888  oddpwdclemodd  12894  oddpwdc  12896  phicl2  12936  phibndlem  12938  phibnd  12939  hashdvds  12943  crth  12946  phimullem  12947  eulerthlemfi  12950  eulerthlemrprm  12951  eulerthlema  12952  hashgcdeq  12962  phisum  12963  oddprm  12982  prm23ge5  12987  pythagtriplem1  12988  pythagtriplem4  12991  pythagtriplem12  12998  pythagtriplem14  13000  pczpre  13020  pcadd  13063  pcmpt  13066  pockthlem  13079  pockthi  13081  infpnlem2  13083  gzreim  13102  4sqlem11  13124  4sqlem12  13125  4sqlem13m  13126  4sqlem17  13130  2expltfac  13162  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilem4  13185  evenennn  13228  ennnfonelemjn  13237  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemnn0  13257  exmidunben  13261  ctinfomlemom  13262  ssnnctlemct  13281  nninfdc  13288  slotex  13323  setscom  13336  strslfv3  13342  setsslid  13347  bassetsnn  13353  basmex  13356  basmexd  13357  relelbasov  13359  ressbas2d  13365  ressbasid  13367  strressid  13368  ressval3d  13369  2strbas1g  13420  2strop1g  13421  rngbaseg  13433  rngplusgg  13434  rngmulrg  13435  srngbased  13444  srngplusgd  13445  srngmulrd  13446  srnginvld  13447  lmodbased  13462  lmodplusgd  13463  lmodscad  13464  lmodvscad  13465  ipsbased  13474  ipsaddgd  13475  ipsmulrd  13476  ipsscad  13477  ipsvscad  13478  ipsipd  13479  topgrpbasd  13494  topgrpplusgd  13495  topgrptsetd  13496  tgvalex  13560  imasex  13569  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  imasaddfn  13581  imasaddval  13582  imasaddf  13583  imasmulfn  13584  imasmulval  13585  imasmulf  13586  qusval  13587  qusex  13589  qusaddvallemg  13597  qusaddflemg  13598  qusaddval  13599  qusaddf  13600  qusmulval  13601  qusmulf  13602  xpsfval  13612  plusffvalg  13625  grpidvalg  13636  igsumvalx  13652  gsumfzval  13654  gsumress  13658  gsum0g  13659  gsumval2  13660  issubmnd  13703  ress0g  13704  ismhm  13716  mhmex  13717  issubm  13727  0mhm  13741  grppropstrg  13774  grpinvfvalg  13797  grpinvval  13798  grpinvfng  13799  grpsubfvalg  13800  grpsubval  13801  grpressid  13816  grplactfval  13856  qusgrp2  13866  mulgfvalg  13874  mulgex  13876  mulgnngsum  13880  issubg  13926  subgex  13929  subgmulg  13941  issubg2m  13942  releqgg  13973  eqgex  13974  eqgfval  13975  eqgen  13980  isghm  13996  ablressid  14088  gfsumsn  14107  gfsump1  14108  prdsex  14114  prdsval  14115  prdsbaslemss  14116  prdsbas  14118  prdsplusg  14119  prdsmulr  14120  xpsval  14143  pwsbas  14147  pwselbasb  14148  pwssnf1o  14153  mgptopng  14168  rngressid  14193  qusrng  14197  dfur2g  14205  ringidss  14272  ring1  14302  ringressid  14306  qusring2  14309  opprringb  14324  dvdsrvald  14338  dvdsrex  14343  unitgrp  14361  unitabl  14362  invrfvald  14367  unitlinv  14371  unitrinv  14372  dvrfvald  14378  rdivmuldivd  14389  invrpropdg  14394  rhmunitinv  14423  isnzr2  14429  issubrng  14445  issubrg  14467  subrgugrp  14486  subrgpropd  14499  rrgmex  14507  aprval  14529  aprprop  14539  islmod  14565  scaffvalg  14580  lssex  14628  lssmex  14629  lsssetm  14630  islssmg  14632  islss3  14653  lspfval  14662  lspval  14664  lspcl  14665  lspex  14669  sralemg  14712  srascag  14716  sravscag  14717  sraipg  14718  sraex  14720  rlmsubg  14732  rlmvnegg  14739  ixpsnbasval  14740  lidlvalg  14745  rspvalg  14746  lidlex  14747  rspex  14748  lidlmex  14749  lidlss  14750  lidlrsppropdg  14769  2idlmex  14775  qusrhm  14802  znlidl  14908  zncrng2  14909  znval  14910  znle  14911  znbaslemnn  14913  znbas  14918  znzrh2  14920  znzrhval  14921  znzrhfo  14922  zndvds  14923  znfi  14929  znhash  14930  znidom  14931  znidomb  14932  psrval  14940  psrbasg  14955  psrelbas  14956  psrplusgg  14959  psraddcl  14961  psr0cl  14962  psrnegcl  14964  psr1clfi  14969  mplvalcoe  14971  mplplusgg  14984  toponsspwpwg  15013  topgele  15020  istps  15023  topontopn  15028  tgclb  15056  lmfval  15184  lmres  15239  ispsmet  15314  psmetge0  15322  ismet  15335  isxmet  15336  xmetge0  15356  isxms2  15443  comet  15490  bdxmet  15492  cnmetdval  15520  cnbl0  15525  cnblcld  15526  reopnap  15537  tgioo  15545  cncfcncntop  15584  cncfmpt2fcntop  15590  maxcncf  15606  mincncf  15607  hovergt0  15641  limcimolemlt  15655  cnplimcim  15658  cnplimclemr  15660  limccnpcntop  15666  limccnp2lem  15667  limccnp2cntop  15668  dvfvalap  15672  dvbss  15676  dvcnp2cntop  15690  dvcn  15691  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvrecap  15704  dvmptfsum  15716  dveflem  15717  plyval  15723  plycolemc  15749  dvply2  15758  reeff1olem  15762  pilem3  15774  ef2kpi  15797  efper  15798  sinperlem  15799  efimpi  15810  ptolemy  15815  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  cosq14gt0  15823  tangtx  15829  sinkpi  15838  coskpi  15839  cosordlem  15840  rplogcl  15870  logge0  15871  logdivlti  15872  logbleb  15952  logblt  15953  binom4  15970  wilthlem1  15974  1sgmprm  15988  1sgm2ppw  15989  mersenne  15991  perfect1  15992  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgsval2lem  16009  lgsval4a  16021  lgsneg  16023  lgsdilem  16026  lgsdirprm  16033  lgsdirnn0  16046  gausslemma2dlem0i  16056  gausslemma2dlem6  16066  gausslemma2dlem7  16067  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgsquadlemofi  16075  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem2  16081  lgsquad2  16082  m1lgs  16084  2lgs  16103  2lgsoddprmlem2  16105  2lgsoddprm  16112  2sqlem2  16114  vtxvalg  16137  vtxex  16139  struct2slots2dom  16159  structvtxval  16160  structiedg0val  16161  structgrssvtx  16163  structgrssiedg  16164  edgstruct  16185  vdegp1bid  16436  wlkv0  16490  upgr2wlkdc  16498  clwwlkex  16519  clwwlkccatlem  16521  eupthfi  16572  trlsegvdeglem6  16586  konigsberglem1  16609  konigsberglem5  16613  depindlem1  16627  pwf1oexmid  16899  nnnninfex  16926  repiecege0  16937  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963