MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3anbrc Unicode version

Theorem syl3anbrc 1180
Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
Hypotheses
Ref Expression
syl3anbrc.1
syl3anbrc.2
syl3anbrc.3
syl3anbrc.4
Assertion
Ref Expression
syl3anbrc

Proof of Theorem syl3anbrc
StepHypRef Expression
1 syl3anbrc.1 . . 3
2 syl3anbrc.2 . . 3
3 syl3anbrc.3 . . 3
41, 2, 33jca 1176 . 2
5 syl3anbrc.4 . 2
64, 5sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\w3a 973
This theorem is referenced by:  soisores  6223  limuni3  6687  onfununi  7031  smores2  7044  smoiso  7052  oelimcl  7268  iserd  7356  erinxp  7404  resixp  7524  undifixp  7525  alephval3  8512  fpwwe2lem12  9040  canthwelem  9049  canthwe  9050  r1limwun  9135  wunex2  9137  tskcard  9180  gruina  9217  nqerf  9329  nqerid  9332  eluzuzle  11118  uztrn  11126  nn0pzuz  11167  zsupss  11200  nn0ge2m1nnALT  11205  xov1plusxeqvd  11695  ige2m1fz  11797  0elfz  11802  elfz0addOLD  11805  uzsubfz0  11811  elfzmlbm  11813  difelfzle  11817  difelfznle  11818  elfzolt2b  11839  elfzolt3b  11840  elfzouz2  11842  fzossrbm1  11854  elfzo0  11863  eluzgtdifelfzo  11878  elfzodifsumelfzo  11882  fzonn0p1  11892  fzonn0p1p1  11894  elfzom1p1elfzo  11895  fzo0sn0fzo1  11902  ssfzo12bi  11907  ubmelm1fzo  11908  elfzonelfzo  11912  fzosplitprm1  11919  fzostep1  11922  injresinjlem  11925  flword2  11949  uzsup  11990  fsuppmapnn0fiub  12097  suppssfz  12100  fzsdom2  12486  ccatval1  12595  ccatrn  12606  ccatw2s1p1  12640  swrdn0  12655  swrdtrcfv  12668  swrdtrcfv0  12669  swrdeq  12671  swrdsymbeq  12672  swrdtrcfvl  12675  swrdswrd  12685  swrdccatwrd  12693  wrdeqs1cat  12700  swrdccatin1  12708  swrdccat3  12717  swrdccatid  12722  repswswrd  12756  cshwidxmod  12774  cshw1  12790  cshwcsh2id  12796  swrds2  12883  2swrd2eqwrdeq  12891  ccat2s1fvwALT  12893  rexuzre  13185  limsupgre  13304  rlimclim1  13368  rlimclim  13369  climrlim2  13370  isercolllem1  13487  isercoll  13490  climcndslem1  13661  tanhbnd  13896  sinbnd2  13917  cosbnd2  13918  rpnnen2  13959  bitsfzolem  14084  bitsfzo  14085  bitsmod  14086  bitsfi  14087  bitsinv1lem  14091  bitsinv1  14092  smueqlem  14140  prmn2uzge3  14237  zgz  14451  gznegcl  14453  gzcjcl  14454  gzaddcl  14455  gzmulcl  14456  vdwlem9  14507  cshwshashlem2  14581  ismred  14999  isfuncd  15234  homdmcoa  15394  isdrs2  15568  fpwipodrs  15794  ipodrsima  15795  psss  15844  psssdm2  15845  sgrp2rid2ex  16045  subgid  16203  issubg2  16216  subsubg  16224  gaorber  16346  orbsta  16351  pmtrfconj  16491  psgnunilem2  16520  psgnunilem3  16521  psgnunilem4  16522  pgpfi1  16615  subgpgp  16617  pgpssslw  16634  subgslw  16636  sylow2alem2  16638  fislw  16645  sylow3lem3  16649  efgs1  16753  efgsp1  16755  efgsres  16756  efgredleme  16761  efgcpbllemb  16773  lt6abl  16897  telgsumfzs  17018  ablfac1eu  17124  isringd  17233  ringsrg  17237  ring1  17248  prdsringd  17261  subrgsubg  17435  islmodd  17518  islssd  17582  islss4  17608  gsummoncoe1  18346  gzrngunit  18483  expmhm  18485  zringunit  18520  zrngunit  18521  prmirredlem  18523  prmirredlemOLD  18526  znidomb  18600  isphld  18689  ocvocv  18702  ocvlss  18703  frlmlbs  18831  mp2pm2mplem4  19310  chfacfisf  19355  chfacfisfcpmat  19356  chfacfscmulfsupp  19360  chfacfpmmulfsupp  19364  chfacfpmmulgsum2  19366  2ndcctbss  19956  finlocfin  20021  dissnlocfin  20030  locfindis  20031  locfincf  20032  isfild  20359  infil  20364  neifil  20381  flimfcls  20527  istgp2  20590  oppgtmd  20596  oppgtgp  20597  distgp  20598  indistgp  20599  symgtgp  20600  submtmd  20603  subgtgp  20604  qustgplem  20619  prdstmdd  20622  prdstgpd  20623  tlmtgp  20698  isngp4  21131  subgngp  21149  ngptgp  21150  tngngp2  21166  nrgtrg  21198  nrgtdrg  21201  elii2  21436  icopnfcnv  21442  xrhmeo  21446  lebnumii  21466  phtpcer  21495  reparpht  21498  phtpcco2  21499  pcohtpy  21520  pcoass  21524  pcorevlem  21526  pi1cpbl  21544  pi1grplem  21549  isclmi  21577  cphsubrglem  21624  cphclm  21636  tchclm  21675  tchcph  21680  clsocv  21690  pjthlem2  21853  ovolf  21893  iundisj2  21959  vitalilem2  22018  vitali  22022  itg2monolem3  22159  dvfsumlem1  22427  dvfsumlem3  22429  mon1puc1p  22551  uc1pmon1p  22552  ply1remlem  22563  drnguc1p  22571  plyaddlem1  22610  coeidlem  22634  aannenlem2  22725  radcnvcl  22812  pilem2  22847  coseq00topi  22895  coseq0negpitopi  22896  tangtx  22898  tanabsge  22899  cosq14gt0  22903  cosq14ge0  22904  cosordlem  22918  sinord  22921  resinf1o  22923  tanord1  22924  tanord  22925  efif1olem3  22931  efsubm  22938  relogrn  22949  logimclad  22960  logrnaddcl  22962  logneg  22972  logcj  22991  argregt0  22995  argrege0  22996  argimgt0  22997  argimlt0  22998  logimul  22999  logneg2  23000  logdmnrp  23022  logcnlem4  23026  dvloglem  23029  logf1o2  23031  efopnlem2  23038  cxpsqrtlem  23083  asinneg  23217  asinsin  23223  acoscos  23224  acosbnd  23231  atancj  23241  atanlogaddlem  23244  atanlogsublem  23246  atanlogsub  23247  atantan  23254  atanbndlem  23256  atans2  23262  leibpi  23273  scvxcvx  23315  jensenlem2  23317  emcllem7  23331  basellem1  23354  ppisval  23377  chtdif  23432  ppidif  23437  ppiub  23479  chtublem  23486  chtub  23487  lgsdilem2  23606  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  2sqlem3  23641  chebbnd1lem1  23654  chebbnd1lem2  23655  chebbnd1lem3  23656  dchrisumlem2  23675  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  dchrisum0flblem2  23694  mulog2sumlem2  23720  logdivbnd  23741  pntpbnd2  23772  pntibndlem1  23774  pntibnd  23778  pntlemc  23780  pntlemg  23783  pntlemq  23786  pntlemf  23790  padicabvf  23816  padicabvcxp  23817  ostth2  23822  ttgcontlem1  24188  axpaschlem  24243  nbgraf1olem5  24445  cyclnspth  24631  wwlknred  24723  wwlknredwwlkn  24726  wwlkextproplem3  24743  clwlkisclwwlklem2fv1  24782  clwlkisclwwlklem2fv2  24783  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkel  24793  clwwlkf  24794  wwlkext2clwwlk  24803  clwwisshclwwlem1  24805  clwwisshclwwlem  24806  erclwwlkref  24813  usg2cwwkdifex  24821  clwlkfclwwlk1hash  24842  clwlkfclwwlk  24844  eupath2lem3  24979  extwwlkfablem2  25078  numclwlk2lem2f  25103  frgrareggt1  25116  grpoinvf  25242  strlem3a  27171  hstrlem3a  27179  iundisj2f  27449  fcoinver  27460  ssnnssfz  27597  bcm1n  27600  iundisj2fi  27602  fsumrp0cl  27685  submomnd  27700  lmodslmd  27747  suborng  27805  locfinreflem  27843  locfinref  27844  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  rnlogbval  28016  nnlogbexp  28020  esumc  28062  esumle  28065  esumlef  28070  esumpinfsum  28083  esumpcvgval  28084  voliune  28201  volfiniune  28202  sibfinima  28281  eulerpartlemt  28310  fiblem  28337  fibp1  28340  dstrvprob  28410  ballotlemsel1i  28451  ballotlemfrceq  28467  eluzmn  28491  plymulx0  28504  signstfvc  28531  signstfveq0  28534  erdszelem4  28638  erdszelem8  28642  txsconlem  28685  cvxscon  28688  cvmliftpht  28763  snmlff  28774  elmrsubrn  28880  msrf  28902  mthmpps  28942  sinccvglem  29038  fallfacval4  29165  areacirc  30112  trer  30134  nnubfi  30243  prter1  30620  nacsfix  30644  eldioph2lem1  30693  irrapxlem1  30758  rmxypairf1o  30847  jm2.27a  30947  hbtlem2  31073  hbt  31079  cntzsdrg  31151  hashgcdlem  31157  mon1pid  31165  mon1psubm  31166  binomcxplemnotnn0  31261  elfzfzo  31458  monoords  31496  fmul01lt1lem2  31579  sumnnodd  31636  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  iblsplit  31765  iblspltprt  31772  itgspltprt  31778  stoweidlem11  31793  stoweidlem17  31799  fourierdlem12  31901  fourierdlem20  31909  fourierdlem25  31914  fourierdlem37  31926  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem54  31943  fourierdlem64  31953  fourierdlem73  31962  fourierdlem79  31968  fourierdlem102  31991  fourierdlem111  32000  fourierdlem114  32003  etransclem23  32040  etransclem48  32065  2elfz2melfz  32334  elfzlble  32336  el2fzo  32339  fzoopth  32340  lswn0  32343  ringrng  32685  isringrng  32687  lidlrng  32733  ssnn0ssfz  32938  lmod1  33093  bnj944  33996  bnj998  34014  bnj1136  34053  bnj1408  34092  lkrlss  34820  diaf11N  36776  dibf11N  36888  lclkr  37260  lclkrs  37266  lcfrlem9  37277  lcfr  37312  mapd1o  37375  hdmapf1oN  37595  hgmapf1oN  37633
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator