MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl31anc Structured version   Visualization version   GIF version

Theorem syl31anc 1320
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl31anc.5 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
Assertion
Ref Expression
syl31anc (𝜑𝜂)

Proof of Theorem syl31anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1234 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl31anc.5 . 2 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
74, 5, 6syl2anc 690 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032
This theorem is referenced by:  syl32anc  1325  stoic4b  1693  elovmpt3rab1  6764  smo11  7321  omeulem2  7523  oeeui  7542  oaabs2  7585  omabs  7587  omxpenlem  7919  map2xp  7988  mapdom2  7989  fsuppsssupp  8147  cantnflt  8425  cnfcom  8453  mapcdaen  8862  pwsdompw  8882  cofsmo  8947  fin1a2lem4  9081  ltmul12a  10724  lt2msq1  10752  ledivp1  10770  lemul1ad  10808  lemul2ad  10809  supaddc  10833  supadd  10834  supmul1  10835  supmul  10838  rpnnen1lem3  11644  rpnnen1lem5  11646  rpnnen1lem3OLD  11650  rpnnen1lem5OLD  11652  lediv2ad  11722  xaddge0  11913  xadddi  11950  xadddi2  11952  supicc  12143  supiccub  12144  supicclub  12145  difelfznle  12273  flval3  12429  fseqsupubi  12590  expcan  12726  ltexp2  12727  ltexp2r  12730  expubnd  12734  ltexp2rd  12846  ltexp2d  12851  leexp2d  12852  expcand  12853  swrdid  13222  swrd0fv  13233  swrds1  13245  ccatswrd  13250  swrdccat2  13252  swrdccatin2  13280  swrdccatin12lem2  13282  swrdccatin12lem3  13283  splfv1  13299  cshwidxmod  13342  wrdl3s3  13495  o1fsum  14328  mertenslem1  14397  eftlub  14620  rpnnen2lem4  14727  ruclem12  14751  dvdsadd  14804  3dvds  14832  3dvdsOLD  14833  divalgmod  14909  divalgmodOLD  14910  bitsmod  14938  bitsinv1lem  14943  bezoutlem4  15039  gcdzeq  15051  rplpwr  15056  sqgcd  15058  bezoutr  15061  rpmulgcd2  15150  rpdvds  15154  coprmproddvdslem  15156  isprm5  15199  divgcdodd  15202  divnumden  15236  crth  15263  phimullem  15264  modprm0  15290  modprmn0modprm0  15292  coprimeprodsq2  15294  pythagtriplem19  15318  pockthlem  15389  prmunb  15398  prmreclem3  15402  prmreclem6  15405  ramub  15497  ramz  15509  pmtrprfv  17638  pmtrprfv3  17639  mndodcong  17726  odngen  17757  pgpfi  17785  pgpssslw  17794  sylow2blem3  17802  lsmless1  17839  lsmless2  17840  lsmless12  17841  lsmmod2  17854  pj1id  17877  odadd2  18017  gexexlem  18020  ablfacrplem  18229  ablfacrp  18230  ablfac1b  18234  ablfac1eu  18237  pgpfac1lem2  18239  kerf1hrm  18508  lsmssspx  18851  lspsncv0  18909  coe1subfv  19399  coe1fzgsumdlem  19434  znunit  19672  uvcvvcl2  19884  uvcvv1  19885  uvcvv0  19886  scmate  20073  mdetunilem2  20176  pmatcoe1fsupp  20263  mat2pmatlin  20297  decpmatmullem  20333  pmatcollpw1lem1  20336  pmatcollpw1lem2  20337  pm2mpghm  20378  chpscmat  20404  chp0mat  20408  chpidmat  20409  cpmadugsumlemB  20436  cpmadugsumlemC  20437  cpmadugsumlemF  20438  clsndisj  20627  neiptopnei  20684  rnelfm  21505  fmfnfmlem2  21507  fmfnfm  21510  flimss1  21525  isfcf  21586  cnextfun  21616  cnextfvval  21617  cnextf  21618  cnextcn  21619  cnextfres1  21620  ustuqtop1  21793  utopsnneiplem  21799  xblss2ps  21953  xblss2  21954  stdbdxmet  22067  metcnpi3  22098  metustexhalf  22108  nmoi  22270  nmoi2  22272  nmoco  22279  blcvx  22337  icccmplem2  22362  icccmplem3  22363  reconnlem2  22366  xrge0gsumle  22372  metds0  22388  metdstri  22389  metdseq0  22392  lebnumlem3  22497  nmoleub2lem  22649  bcthlem5  22846  minveclem2  22918  minveclem3b  22920  minveclem4  22924  minveclem6  22926  icombl  23052  cncombf  23144  mbflimsup  23152  itg2monolem1  23236  itg2mono  23239  itg2cnlem1  23247  itg2cnlem2  23248  bddmulibl  23324  ellimc2  23360  cpnord  23417  cpnres  23419  dvmulbr  23421  dvcobr  23428  dvlipcn  23474  dvlip2  23475  c1liplem1  23476  dvivthlem1  23488  lhop1lem  23493  lhop1  23494  dvfsumlem2  23507  itgsubstlem  23528  deg1add  23580  deg1sublt  23587  ply1remlem  23639  plyeq0lem  23683  taylthlem2  23845  ulmdvlem3  23873  abelthlem7  23909  pilem2  23923  pilem3  23924  pige3  23986  logccv  24122  cxpaddlelem  24205  cvxcl  24424  fsumharmonic  24451  ftalem5  24516  dvdsmulf1o  24633  bposlem1  24722  lgsqr  24789  lgsquad2lem2  24823  2lgsoddprmlem1  24846  2sqlem8a  24863  2sqlem8  24864  dchrmusum2  24896  dchrvmasumiflem1  24903  dchrisum0flblem1  24910  dchrisum0lem1b  24917  pntlem3  25011  tgdim01  25115  axsegcon  25521  ax5seglem1  25522  ax5seglem2  25523  axlowdimlem6  25541  axeuclidlem  25556  axcontlem7  25564  axcontlem9  25566  axcontlem10  25567  cusgrasize2inds  25767  usgra2adedgspth  25903  vdgrun  26190  vdgrfiun  26191  vdgr1d  26192  vdgr1b  26193  vdgr1a  26195  2pthfrgra  26300  vdn1frgrav2  26314  vdgn1frgrav2  26315  frgrawopreg  26338  frrusgraord  26360  numclwwlk2lem1  26391  numclwwlk3  26398  frgrareg  26406  nmoub3i  26814  ubthlem3  26914  minvecolem2  26917  minvecolem4  26922  minvecolem5  26923  minvecolem6  26924  htthlem  26960  pjpjpre  27464  chscllem1  27682  chscllem2  27683  chscllem3  27684  cnlnadjlem2  28113  leopnmid  28183  br8d  28604  ogrpaddlt  28851  archirngz  28876  ornglmullt  28940  orngrmullt  28941  elrhmunit  28953  qqhval2lem  29155  qqhnm  29164  qqhucn  29166  esumcst  29254  esumpcvgval  29269  measunl  29408  dya2iocbrsiga  29466  dya2icobrsiga  29467  omssubadd  29491  inelcarsg  29502  carsgclctunlem2  29510  sibfof  29531  sitgaddlemb  29539  oddpwdc  29545  eulerpartlemgc  29553  bayesth  29630  erdszelem8  30236  br8  30701  matunitlindflem2  32375  totbndbnd  32557  prdsbnd  32561  rrncmslem  32600  rrntotbnd  32604  isdrngo2  32726  lsatcmp  33107  lcvexchlem2  33139  lcvexchlem3  33140  ncvr1  33376  cvrletrN  33377  cvrnbtwn3  33380  cvrnrefN  33386  cvrcmp  33387  0ltat  33395  atnle0  33413  atlen0  33414  cvlcvr1  33443  cvrval3  33516  atle  33539  athgt  33559  1cvratex  33576  ps-2  33581  ps-2b  33585  llnnleat  33616  2atneat  33618  llnle  33621  atcvrlln  33623  llncmp  33625  2llnmat  33627  2at0mat0  33628  2atm  33630  ps-2c  33631  lplnle  33643  lplnnle2at  33644  llncvrlpln2  33660  llncvrlpln  33661  2lplnmN  33662  2llnmj  33663  2atmat  33664  lplncmp  33665  lplnexllnN  33667  2llnm2N  33671  2llnm4  33673  lvolnle3at  33685  4atlem3a  33700  4atlem3b  33701  4atlem10  33709  4atlem11  33712  4atlem12  33715  lplncvrlvol2  33718  lplncvrlvol  33719  lvolcmp  33720  2lplnm2N  33724  2lplnmj  33725  dalempjsen  33756  dalemcea  33763  dalem2  33764  dalemdea  33765  dalem9  33775  dalem16  33782  dalemcjden  33795  dalem21  33797  dalem23  33799  dalem39  33814  dalem54  33829  dalem60  33835  cdlemb  33897  elpadd2at  33909  paddasslem4  33926  paddasslem7  33929  paddasslem15  33937  paddasslem16  33938  pmodlem1  33949  pmodlem2  33950  llnexchb2  33972  pclfinclN  34053  osumcllem9N  34067  pmapojoinN  34071  pexmidN  34072  pl42lem1N  34082  lhp0lt  34106  lhpexle1  34111  lhpexle2lem  34112  lhpexle3lem  34114  lhprelat3N  34143  ltrnid  34238  trlval3  34291  arglem1N  34294  cdlemc5  34299  cdleme3b  34333  cdleme3c  34334  cdleme3h  34339  cdleme7e  34351  cdleme7ga  34352  cdleme20l1  34425  cdleme20l2  34426  cdleme20l  34427  cdleme22b  34446  cdlemefrs29clN  34504  cdlemefrs32fva  34505  cdlemeg46fvcl  34611  cdlemeg46c  34618  cdlemeg46fvaw  34621  cdlemeg46req  34634  cdleme48fgv  34643  cdlemf1  34666  cdlemg1cex  34693  cdlemg2dN  34695  cdlemg2ce  34697  cdlemg12e  34752  cdlemg35  34818  cdlemh  34922  tendocan  34929  cdlemk28-3  35013  tendoex  35080  dih1  35392  dihmeetlem9N  35421  dihlspsnssN  35438  dihlspsnat  35439  lcfrlem23  35671  mzpsubst  36128  rencldnfi  36202  irrapx1  36209  pellexlem3  36212  pellexlem5  36214  infmrgelbi  36259  pellqrex  36260  pellfundge  36263  rmspecfund  36291  congtr  36349  acongeq  36367  jm2.20nn  36381  jm2.25lem1  36382  jm2.26  36386  expdiophlem1  36405  hbtlem2  36512  suprubd  37281  suprleubrd  37287  suprlubrd  37291  suprnmpt  38149  wessf1ornlem  38165  mpct  38187  upbdrech  38259  ssfiunibd  38263  uzfissfz  38283  xleadd2d  38284  suprltrp  38285  xleadd1d  38286  iccintsng  38396  limcrecl  38496  fnlimfvre  38541  dvmulcncf  38615  dvdivcncf  38617  dvbdfbdioolem1  38618  ioodvbdlimc1lem2  38622  ioodvbdlimc2lem  38624  stoweidlem1  38694  stoweidlem20  38713  stoweidlem24  38717  stoweidlem34  38727  stoweidlem45  38738  stoweidlem60  38753  fourierdlem20  38820  fourierdlem31  38831  fourierdlem38  38838  fourierdlem64  38863  fourierdlem79  38878  fourierdlem94  38893  fourierdlem113  38912  fouriersw  38924  fouriercn  38925  sge0isum  39120  hoicvr  39238  ovnsubaddlem2  39261  hoidmv1lelem1  39281  hoidmv1lelem3  39283  hoidmvlelem1  39285  hoidmvlelem4  39288  smflimlem2  39458  fmtnof1  39786  lighneallem2  39862  pfxfv  40063  nbupgr  40564  nbumgrvtx  40566  cusgrsize2inds  40667  upgr1wlkwlk  40845  2pthnloop  40935  frgrwopreg  41484  frrusgrord  41502  av-numclwwlk2lem1  41530  av-frgrareg  41546  lincresunit3  42062  elbigolo1  42147
  Copyright terms: Public domain W3C validator