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

Theorem syl31anc 1369
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 1261 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl31anc.5 . 2 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
74, 5, 6syl2anc 694 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  syl32anc  1374  stoic4b  1743  elovmpt3rab1  6935  smo11  7506  omeulem2  7708  oeeui  7727  oaabs2  7770  omabs  7772  omxpenlem  8102  map2xp  8171  mapdom2  8172  fsuppsssupp  8332  cantnflt  8607  cnfcom  8635  mapcdaen  9044  pwsdompw  9064  cofsmo  9129  fin1a2lem4  9263  ltmul12a  10917  lt2msq1  10945  ledivp1  10963  lemul1ad  11001  lemul2ad  11002  suprubd  11023  supaddc  11028  supadd  11029  supmul1  11030  supmul  11033  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  lediv2ad  11932  xaddge0  12126  xadddi  12163  xadddi2  12165  supicc  12358  supiccub  12359  supicclub  12360  difelfznle  12492  flval3  12656  expcan  12953  ltexp2  12954  ltexp2r  12957  expubnd  12961  ltexp2rd  13073  ltexp2d  13078  leexp2d  13079  expcand  13080  swrdid  13474  swrd0fv  13485  swrds1  13497  ccatswrd  13502  swrdccat2  13504  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12lem3  13536  splfv1  13552  cshwidxmod  13595  wrdl3s3  13751  o1fsum  14589  mertenslem1  14660  eftlub  14883  rpnnen2lem4  14990  ruclem12  15014  dvdsadd  15071  3dvds  15099  3dvdsOLD  15100  divalgmod  15176  divalgmodOLD  15177  bitsmod  15205  bitsinv1lem  15210  bezoutlem4  15306  gcdzeq  15318  rplpwr  15323  sqgcd  15325  bezoutr  15328  rpmulgcd2  15417  rpdvds  15421  coprmproddvdslem  15423  isprm5  15466  divgcdodd  15469  divnumden  15503  crth  15530  phimullem  15531  modprm0  15557  modprmn0modprm0  15559  coprimeprodsq2  15561  pythagtriplem19  15585  pockthlem  15656  prmunb  15665  prmreclem3  15669  prmreclem6  15672  ramub  15764  ramz  15776  pmtrprfv  17919  pmtrprfv3  17920  mndodcong  18007  odngen  18038  pgpfi  18066  pgpssslw  18075  sylow2blem3  18083  lsmless1  18120  lsmless2  18121  lsmless12  18122  lsmmod2  18135  pj1id  18158  odadd2  18298  gexexlem  18301  ablfacrplem  18510  ablfacrp  18511  ablfac1b  18515  ablfac1eu  18518  pgpfac1lem2  18520  kerf1hrm  18791  lsmssspx  19136  lspsncv0  19194  coe1subfv  19684  coe1fzgsumdlem  19719  znunit  19960  uvcvvcl2  20175  uvcvv1  20176  uvcvv0  20177  scmate  20364  mdetunilem2  20467  pmatcoe1fsupp  20554  mat2pmatlin  20588  decpmatmullem  20624  pmatcollpw1lem1  20627  pmatcollpw1lem2  20628  pm2mpghm  20669  chpscmat  20695  chp0mat  20699  chpidmat  20700  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  clsndisj  20927  neiptopnei  20984  rnelfm  21804  fmfnfmlem2  21806  fmfnfm  21809  flimss1  21824  isfcf  21885  cnextfun  21915  cnextfvval  21916  cnextf  21917  cnextcn  21918  cnextfres1  21919  ustuqtop1  22092  utopsnneiplem  22098  xblss2ps  22253  xblss2  22254  stdbdxmet  22367  metcnpi3  22398  metustexhalf  22408  nmoi  22579  nmoi2  22581  nmoco  22588  blcvx  22648  icccmplem2  22673  icccmplem3  22674  reconnlem2  22677  xrge0gsumle  22683  metds0  22700  metdstri  22701  metdseq0  22704  lebnumlem3  22809  nmoleub2lem  22960  bcthlem5  23171  minveclem2  23243  minveclem3b  23245  minveclem4  23249  minveclem6  23251  icombl  23378  cncombf  23470  mbflimsup  23478  itg2monolem1  23562  itg2mono  23565  itg2cnlem1  23573  itg2cnlem2  23574  bddmulibl  23650  ellimc2  23686  cpnord  23743  cpnres  23745  dvmulbr  23747  dvcobr  23754  dvlipcn  23802  dvlip2  23803  c1liplem1  23804  dvivthlem1  23816  lhop1lem  23821  lhop1  23822  dvfsumlem2  23835  itgsubstlem  23856  deg1add  23908  deg1sublt  23915  ply1remlem  23967  plyeq0lem  24011  taylthlem2  24173  ulmdvlem3  24201  abelthlem7  24237  pilem2  24251  pilem3  24252  pige3  24314  logccv  24454  cxpaddlelem  24537  cvxcl  24756  fsumharmonic  24783  ftalem5  24848  dvdsmulf1o  24965  bposlem1  25054  lgsqr  25121  lgsquad2lem2  25155  2lgsoddprmlem1  25178  2sqlem8a  25195  2sqlem8  25196  dchrmusum2  25228  dchrvmasumiflem1  25235  dchrisum0flblem1  25242  dchrisum0lem1b  25249  pntlem3  25343  tgdim01  25447  axsegcon  25852  ax5seglem1  25853  ax5seglem2  25854  axlowdimlem6  25872  axeuclidlem  25887  axcontlem7  25895  axcontlem9  25897  axcontlem10  25898  nbupgr  26285  nbumgrvtx  26287  cusgrsize2inds  26405  upgriswlk  26593  2pthnloop  26683  clwwlknonex2lem2  27083  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  frgrreg  27381  nmoub3i  27756  ubthlem3  27856  minvecolem2  27859  minvecolem4  27864  minvecolem5  27865  minvecolem6  27866  htthlem  27902  pjpjpre  28406  chscllem1  28624  chscllem2  28625  chscllem3  28626  cnlnadjlem2  29055  leopnmid  29125  br8d  29548  ogrpaddlt  29846  archirngz  29871  ornglmullt  29935  orngrmullt  29936  elrhmunit  29948  qqhval2lem  30153  qqhnm  30162  qqhucn  30164  esumcst  30253  esumpcvgval  30268  measunl  30407  dya2iocbrsiga  30465  dya2icobrsiga  30466  omssubadd  30490  inelcarsg  30501  carsgclctunlem2  30509  sibfof  30530  sitgaddlemb  30538  oddpwdc  30544  eulerpartlemgc  30552  bayesth  30629  ftc2re  30804  breprexplemc  30838  tgoldbachgt  30869  erdszelem8  31306  br8  31772  noetalem3  31990  noetalem5  31992  matunitlindflem2  33536  totbndbnd  33718  prdsbnd  33722  rrncmslem  33761  rrntotbnd  33765  isdrngo2  33887  lsatcmp  34608  lcvexchlem2  34640  lcvexchlem3  34641  ncvr1  34877  cvrletrN  34878  cvrnbtwn3  34881  cvrnrefN  34887  cvrcmp  34888  0ltat  34896  atnle0  34914  atlen0  34915  cvlcvr1  34944  cvrval3  35017  atle  35040  athgt  35060  1cvratex  35077  ps-2  35082  ps-2b  35086  llnnleat  35117  2atneat  35119  llnle  35122  atcvrlln  35124  llncmp  35126  2llnmat  35128  2at0mat0  35129  2atm  35131  ps-2c  35132  lplnle  35144  lplnnle2at  35145  llncvrlpln2  35161  llncvrlpln  35162  2lplnmN  35163  2llnmj  35164  2atmat  35165  lplncmp  35166  lplnexllnN  35168  2llnm2N  35172  2llnm4  35174  lvolnle3at  35186  4atlem3a  35201  4atlem3b  35202  4atlem10  35210  4atlem11  35213  4atlem12  35216  lplncvrlvol2  35219  lplncvrlvol  35220  lvolcmp  35221  2lplnm2N  35225  2lplnmj  35226  dalempjsen  35257  dalemcea  35264  dalem2  35265  dalemdea  35266  dalem9  35276  dalem16  35283  dalemcjden  35296  dalem21  35298  dalem23  35300  dalem39  35315  dalem54  35330  dalem60  35336  cdlemb  35398  elpadd2at  35410  paddasslem4  35427  paddasslem7  35430  paddasslem15  35438  paddasslem16  35439  pmodlem1  35450  pmodlem2  35451  llnexchb2  35473  pclfinclN  35554  osumcllem9N  35568  pmapojoinN  35572  pexmidN  35573  pl42lem1N  35583  lhp0lt  35607  lhpexle1  35612  lhpexle2lem  35613  lhpexle3lem  35615  lhprelat3N  35644  ltrnid  35739  trlval3  35792  arglem1N  35795  cdlemc5  35800  cdleme3b  35834  cdleme3c  35835  cdleme3h  35840  cdleme7e  35852  cdleme7ga  35853  cdleme20l1  35925  cdleme20l2  35926  cdleme20l  35927  cdleme22b  35946  cdlemefrs29clN  36004  cdlemefrs32fva  36005  cdlemeg46fvcl  36111  cdlemeg46c  36118  cdlemeg46fvaw  36121  cdlemeg46req  36134  cdleme48fgv  36143  cdlemf1  36166  cdlemg1cex  36193  cdlemg2dN  36195  cdlemg2ce  36197  cdlemg12e  36252  cdlemg35  36318  cdlemh  36422  tendocan  36429  cdlemk28-3  36513  tendoex  36580  dih1  36892  dihmeetlem9N  36921  dihlspsnssN  36938  dihlspsnat  36939  lcfrlem23  37171  mzpsubst  37628  rencldnfi  37702  irrapx1  37709  pellexlem3  37712  pellexlem5  37714  infmrgelbi  37759  pellqrex  37760  pellfundge  37763  rmspecfund  37791  congtr  37849  acongeq  37867  jm2.20nn  37881  jm2.25lem1  37882  jm2.26  37886  expdiophlem1  37905  hbtlem2  38011  suprleubrd  38783  suprlubrd  38787  suprnmpt  39669  wessf1ornlem  39685  mpct  39707  upbdrech  39833  ssfiunibd  39837  uzfissfz  39855  xleadd2d  39856  suprltrp  39857  xleadd1d  39858  suprleubrnmpt  39962  iccintsng  40067  limcrecl  40179  fnlimfvre  40224  dvmulcncf  40458  dvdivcncf  40460  dvbdfbdioolem1  40461  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweidlem1  40536  stoweidlem20  40555  stoweidlem24  40559  stoweidlem34  40569  stoweidlem45  40580  stoweidlem60  40595  fourierdlem20  40662  fourierdlem31  40673  fourierdlem38  40680  fourierdlem64  40705  fourierdlem79  40720  fourierdlem94  40735  fourierdlem113  40754  fouriersw  40766  fouriercn  40767  sge0isum  40962  hoicvr  41083  ovnsubaddlem2  41106  hoidmv1lelem1  41126  hoidmv1lelem3  41128  hoidmvlelem1  41130  hoidmvlelem4  41133  smflimlem2  41301  pfxfv  41724  fmtnof1  41772  lighneallem2  41848  upgrwlkupwlk  42046  lincresunit3  42595  elbigolo1  42676
  Copyright terms: Public domain W3C validator