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  4222  unipw  4359  opeluu  4598  uniexb  4621  unon  4660  onintrab2im  4667  xpexg  4891  resiexg  5111  imaexg  5143  exse2  5164  soirri  5185  djudisj  5218  elxp5  5279  cnvexg  5328  cnviinm  5332  coexg  5335  funssres  5423  f1oabexg  5654  sefvex  5719  ssimaex  5767  mptfvex  5794  f1ompt  5862  fmptcof  5878  resfunexg  5939  mptexg  5945  funfvima3  5955  ovid  6208  ov  6211  ofres  6321  cofunexg  6342  opabex3d  6354  opabex3  6355  oprabexd  6364  1stcof  6401  2ndcof  6402  mpoexxg  6450  cnvf1o  6465  f2ndf  6466  algrflemg  6470  tposexg  6534  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemibfn  6604  tfrlemi14d  6609  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemres  6625  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemres  6638  rdgtfr  6650  rdgruledefgg  6651  rdgon  6662  frecabex  6674  freccllem  6678  frecfcllem  6680  omcl  6739  oeicl  6740  erth  6858  th3qlem1  6916  mapex  6933  pmvalg  6938  mapfoss  6952  mapsnconst  6982  ixpexgg  7010  fundmen  7100  cnvct  7103  mapsnend  7105  snfig  7109  unen  7111  xpdom2  7135  mapxpen  7154  phplem2  7160  findcard2  7199  findcard2s  7200  infnfi  7205  relcnvfi  7261  sbthlemi8  7288  sbthlemi10  7290  fival  7309  fiss  7316  inl11  7411  casef  7434  caseinj  7435  caseinl  7437  caseinr  7438  djudom  7439  difinfsn  7446  djuinj  7452  0ct  7453  ctmlemr  7454  ctssdccl  7457  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  djuassen  7579  xpdjuen  7580  djudoml  7581  djudomr  7582  cc2lem  7638  ltnnnq  7796  nnnq0lem1  7819  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemfl  7948  mulnqprlemfu  7949  suplocexprlem2b  8087  prsrlem1  8115  gt0srpr  8121  caucvgsrlemcl  8162  caucvgsrlemfv  8164  caucvgsrlembound  8167  mulcnsr  8208  mulcnsrec  8216  addvalex  8217  pitoregt0  8222  axmulass  8246  axdistr  8247  recriota  8263  mulrid  8329  axmulgt0  8403  cnegexlem2  8509  cnegex  8511  gt0ne0d  8847  recexre  8914  msqge0  8952  mulge0  8955  aptap  8986  recgt0  9188  recreclt  9238  cju  9299  nnge1  9336  nnnlt1  9339  nn0nlt0  9600  nnnle0  9702  elz2  9725  nnm1ge0  9741  recnz  9749  zneo  9757  uz3m2nn  9988  eluz2b2  10018  nn01to3  10032  mnflt  10201  xnn0dcle  10220  xltadd1  10294  lincmb01cmp  10421  iccf1o  10423  fz1n  10464  fseq1p1m1  10517  fznn0  10536  fzctr  10556  4fvwrd4  10563  fzo0n  10591  elfzonlteqm1  10644  divfl0  10751  modqelico  10791  zmodfz  10803  modqid  10806  modqmuladdim  10824  m1modge3gt1  10828  addmodid  10829  frec2uzf1od  10863  frecfzennn  10883  frecfzen2  10884  fzfig  10887  ser0  10990  ser3le  10994  expgt1  11034  expubnd  11053  iexpcyc  11101  binom2sub  11110  binom3  11114  zesq  11116  bernneq  11118  bernneq2  11119  expnbnd  11121  expnlbnd2  11123  facdiv  11197  faclbnd2  11201  faclbnd3  11202  bcval4  11211  hashinfom  11238  hashennn  11240  fihashf1rn  11248  isfinite4im  11252  hashfz  11283  ssenneg  11301  hashf1lem1  11306  hashf1lem2  11307  iswrd  11327  iswrdiz  11332  wrdexg  11336  wrdexb  11337  wrdfin  11344  wrdnval  11356  wrdred1hash  11369  ccatsymb  11391  ccatalpha  11402  s111  11420  fzowrddc  11440  swrdlen  11445  swrdwrdsymbg  11457  pfxval  11467  pfx0g  11469  fnpfx  11470  pfxlen  11478  cats1un  11514  swrdccat  11528  crre  11643  crim  11644  remim  11646  mulreap  11650  cjreb  11652  recj  11653  reneg  11654  readd  11655  remullem  11657  imcj  11661  imneg  11662  imadd  11663  cjadd  11670  cjneg  11676  imval2  11680  cjreim  11690  cnrecnv  11697  uzin2  11774  absval  11788  rennim  11789  resqrexlemcalc3  11803  resqrexlemnm  11805  resqrexlemcvg  11806  resqrexlemgt0  11807  resqrexlemga  11810  absreimsq  11854  absreim  11855  amgm2  11906  climconst2  12081  climshft  12094  climshft2  12096  reccn2ap  12103  climge0  12115  sumsnf  12200  sumnul  12215  isumcl  12216  fsum2dlemstep  12225  fisumcom2  12229  fsumabs  12256  fsumiun  12268  binom  12275  bcxmas  12280  arisum  12289  expcnvap0  12293  explecnv  12296  geosergap  12297  geolim  12302  geolim2  12303  geo2sum  12305  geo2lim  12307  cvgratnnlemrate  12321  cvgratz  12323  mertenslemi1  12326  prodf1  12333  prodeq2w  12347  fprodntrivap  12375  prodsnf  12383  fprod2dlemstep  12413  fprodcom2fi  12417  efcllemp  12449  ege2le3  12462  eftlub  12481  efgt1  12488  tanval2ap  12504  tanval3ap  12505  resinval  12506  recosval  12507  efi4p  12508  resin4p  12509  recos4p  12510  resincl  12511  recoscl  12512  efmival  12524  efeul  12525  sinadd  12527  cosadd  12528  tanaddap  12530  sinmul  12535  cos2tsin  12542  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  sin01gt0  12553  cos01gt0  12554  absef  12561  absefib  12562  efieq1re  12563  demoivreALT  12565  eirraplem  12568  3dvds  12655  odd2np1  12664  oddm1even  12666  oddp1even  12667  oexpneg  12668  opoe  12686  omoe  12687  nn0o1gt2  12696  nn0o  12698  bitsdc  12738  bitsfzolem  12745  bitsfzo  12746  bitsinv1lem  12752  bitsinv1  12753  nninfctlemfo  12841  algcvg  12850  algcvgblem  12851  1nprm  12916  1idssfct  12917  oddprmge3  12938  divgcdodd  12946  phicl2  13020  phibndlem  13022  phibnd  13023  hashdvds  13027  crth  13030  phimullem  13031  eulerthlemfi  13034  eulerthlemrprm  13035  eulerthlema  13036  hashgcdeq  13046  phisum  13047  oddprm  13066  prm23ge5  13071  pythagtriplem1  13072  pythagtriplem4  13075  pythagtriplem12  13082  pythagtriplem14  13084  pczpre  13104  pcadd  13147  pcmpt  13150  pockthlem  13163  pockthi  13165  infpnlem2  13167  gzreim  13186  4sqlem11  13208  4sqlem12  13209  4sqlem13m  13210  4sqlem17  13214  2expltfac  13247  prmlem0  13248  prmlem1  13250  prmlem2  13262  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemefi  13294  ballotfilemodife  13297  ballotfilem4  13298  evenennn  13341  ennnfonelemjn  13350  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemnn0  13370  exmidunben  13374  ctinfomlemom  13375  ssnnctlemct  13394  nninfdc  13401  slotex  13436  setscom  13449  strslfv3  13455  setsslid  13460  bassetsnn  13466  basmex  13469  basmexd  13470  relelbasov  13473  ressbas2d  13480  ressbasid  13482  strressid  13483  ressval3d  13484  2strbas1g  13535  2strop1g  13536  rngbaseg  13548  rngplusgg  13549  rngmulrg  13550  srngbased  13559  srngplusgd  13560  srngmulrd  13561  srnginvld  13562  lmodbased  13577  lmodplusgd  13578  lmodscad  13579  lmodvscad  13580  ipsbased  13589  ipsaddgd  13590  ipsmulrd  13591  ipsscad  13592  ipsvscad  13593  ipsipd  13594  topgrpbasd  13609  topgrpplusgd  13610  topgrptsetd  13611  tgvalex  13675  imasex  13684  imasival  13685  imasbas  13686  imasplusg  13687  imasmulr  13688  imasaddfn  13696  imasaddval  13697  imasaddf  13698  imasmulfn  13699  imasmulval  13700  imasmulf  13701  qusval  13702  qusex  13704  qusaddvallemg  13712  qusaddflemg  13713  qusaddval  13714  qusaddf  13715  qusmulval  13716  qusmulf  13717  xpsfval  13727  plusffvalg  13740  grpidvalg  13751  gzsumvalx  13767  gzsumfzval  13769  gzsumress  13770  gzsum0  13771  gzsumval2  13772  issubmnd  13813  ress0g  13814  ismhm  13826  mhmex  13827  issubm  13837  0mhm  13851  grppropstrg  13882  grpinvfvalg  13905  grpinvval  13906  grpinvfng  13907  grpsubfvalg  13908  grpsubval  13909  grpressid  13924  grplactfval  13964  qusgrp2  13974  mulgfvalg  13982  mulgex  13984  mulgnngzsum  13988  issubg  14034  subgex  14037  subgmulg  14049  issubg2m  14050  releqgg  14081  eqgex  14082  eqgfval  14083  eqgen  14088  isghm  14104  cntzex  14149  cntzfval  14151  cntzval  14152  cntz2ss  14167  ablressid  14228  gsumsncmn  14245  gsump1  14246  gsummptfidmadd  14250  gsummptfidmsplit  14253  prdsex  14278  prdsval  14279  prdsbaslemss  14280  prdsbas  14282  prdsplusg  14283  prdsmulr  14284  xpsval  14307  pwsbas  14311  pwselbasb  14312  pwssnf1o  14317  mgptopng  14334  rngressid  14359  qusrng  14363  dfur2g  14372  ringidss  14440  ring1  14470  ringressid  14476  qusring2  14479  opprringb  14494  dvdsrvald  14508  dvdsrex  14513  unitgrp  14531  unitabl  14532  invrfvald  14537  unitlinv  14541  unitrinv  14542  dvrfvald  14548  rdivmuldivd  14559  invrpropdg  14564  rhmunitinv  14593  isnzr2  14599  issubrng  14615  issubrg  14637  subrgugrp  14656  subrgpropd  14669  rrgmex  14677  aprval  14699  aprprop  14709  islmod  14735  scaffvalg  14751  lssex  14799  lssmex  14800  lsssetm  14801  islssmg  14803  islss3  14824  lspfval  14833  lspval  14835  lspcl  14836  lspex  14840  sralemg  14883  srascag  14887  sravscag  14888  sraipg  14889  sraex  14891  rlmsubg  14903  rlmvnegg  14910  ixpsnbasval  14911  lidlvalg  14916  rspvalg  14917  lidlex  14918  rspex  14919  lidlmex  14920  lidlss  14921  lidlrsppropdg  14940  2idlmex  14946  qusrhm  14973  gsumfsum  15031  znlidl  15077  zncrng2  15078  znval  15079  znle  15080  znbaslemnn  15082  znbas  15087  znzrh2  15089  znzrhval  15090  znzrhfo  15091  zndvds  15092  znfi  15098  znhash  15099  znidom  15100  znidomb  15101  aspval  15123  aspsubrg  15126  asclfval  15129  psrval  15160  psrbasg  15187  psrelbas  15188  psrplusgg  15191  psraddcl  15193  psrmulrg  15195  psrmulclfilem  15198  psr0cl  15200  psrnegcl  15202  psr1clfi  15207  psrlidmfi  15208  mvrval2  15216  mvrffi  15218  mplvalg  15222  mplplusgg  15236  toponsspwpwg  15265  topgele  15272  istps  15275  topontopn  15280  tgclb  15308  lmfval  15436  lmres  15491  ispsmet  15566  psmetge0  15574  ismet  15587  isxmet  15588  xmetge0  15608  isxms2  15695  comet  15742  bdxmet  15744  cnmetdval  15772  cnbl0  15777  cnblcld  15778  reopnap  15789  tgioo  15797  cncfcncntop  15836  cncfmpt2fcntop  15842  maxcncf  15858  mincncf  15859  hovergt0  15893  limcimolemlt  15907  cnplimcim  15910  cnplimclemr  15912  limccnpcntop  15918  limccnp2lem  15919  limccnp2cntop  15920  dvfvalap  15924  dvbss  15928  dvcnp2cntop  15942  dvcn  15943  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvrecap  15956  dvmptfsum  15968  dveflem  15969  plyval  15975  plycolemc  16001  dvply2  16010  reeff1olem  16014  pilem3  16027  ef2kpi  16050  efper  16051  sinperlem  16052  efimpi  16063  ptolemy  16068  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  cosq14gt0  16076  tangtx  16082  sinkpi  16091  coskpi  16092  cosordlem  16094  rplogcl  16126  logge0  16127  logdivlti  16128  logbleb  16214  logblt  16215  binom4  16236  log2tlbndlog2  16237  log2ublem2  16239  log2ublog2  16241  birthdaylem2  16243  wilthlem1  16249  ppiqsval  16257  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  ppiqeq0  16297  1sgmprm  16305  1sgm2ppw  16306  ppiublem1  16308  ppiqub  16310  chtqleppi  16311  chtublem  16312  chtqub  16313  mersenne  16314  perfect1  16315  perfectlem1  16316  perfectlem2  16317  perfect  16318  bcmono  16321  bcmax  16322  bclbnd  16324  bpos1lem  16326  bpos1  16327  bposlem1  16328  bposlem2  16329  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgsval2lem  16351  lgsval4a  16363  lgsneg  16365  lgsdilem  16368  lgsdirprm  16375  lgsdirnn0  16388  gausslemma2dlem0i  16398  gausslemma2dlem6  16408  gausslemma2dlem7  16409  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlemofi  16417  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem2  16423  lgsquad2  16424  m1lgs  16426  2lgs  16445  2lgsoddprmlem2  16447  2lgsoddprm  16454  2sqlem2  16456  vtxvalg  16479  vtxex  16481  struct2slots2dom  16501  structvtxval  16502  structiedg0val  16503  structgrssvtx  16505  structgrssiedg  16506  edgstruct  16527  vdegp1bid  16778  wlkv0  16832  upgr2wlkdc  16840  clwwlkex  16861  clwwlkccatlem  16863  eupthfi  16914  trlsegvdeglem6  16928  konigsberglem1  16951  konigsberglem5  16955  depindlem1  16969  pwf1oexmid  17251  nnnninfex  17288  repiecege0  17299  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326