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

Theorem syl3anbrc 1136
Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
Hypotheses
Ref Expression
syl3anbrc.1  |-  ( ph  ->  ps )
syl3anbrc.2  |-  ( ph  ->  ch )
syl3anbrc.3  |-  ( ph  ->  th )
syl3anbrc.4  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
Assertion
Ref Expression
syl3anbrc  |-  ( ph  ->  ta )

Proof of Theorem syl3anbrc
StepHypRef Expression
1 syl3anbrc.1 . . 3  |-  ( ph  ->  ps )
2 syl3anbrc.2 . . 3  |-  ( ph  ->  ch )
3 syl3anbrc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1132 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 203 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  limuni3  4659  soisores  5840  onfununi  6374  smores2  6387  smoiso  6395  oelimcl  6614  iserd  6702  erinxp  6749  resixp  6867  undifixp  6868  alephval3  7753  fpwwe2lem12  8279  canthwelem  8288  canthwe  8289  r1limwun  8374  wunex2  8376  tskcard  8419  gruina  8456  nqerf  8570  nqerid  8573  uztrn  10260  zsupss  10323  xov1plusxeqvd  10796  elfzolt2b  10901  elfzolt3b  10902  elfzouz2  10904  elfzo0  10920  fzostep1  10938  flword2  10959  uzsup  10983  fzsdom2  11398  ccatval1  11447  wrdeqs1cat  11491  swrds2  11576  rexuzre  11852  limsupgre  11971  rlimclim1  12035  rlimclim  12036  climrlim2  12037  isercolllem1  12154  isercoll  12157  climcndslem1  12324  tanhbnd  12457  sinbnd2  12478  cosbnd2  12479  rpnnen2  12520  bitsfzolem  12641  bitsfzo  12642  bitsmod  12643  bitsfi  12644  bitsinv1lem  12648  bitsinv1  12649  smueqlem  12697  zgz  12996  gznegcl  12998  gzcjcl  12999  gzaddcl  13000  gzmulcl  13001  vdwlem9  13052  ismred  13520  isfuncd  13755  homdmcoa  13915  isdrs2  14089  fpwipodrs  14283  ipodrsima  14284  psss  14339  psssdm2  14340  subgid  14639  issubg2  14652  subsubg  14656  gaorber  14778  orbsta  14783  pgpfi1  14922  subgpgp  14924  pgpssslw  14941  subgslw  14943  sylow2alem2  14945  fislw  14952  sylow3lem3  14956  efgs1  15060  efgsp1  15062  efgsres  15063  efgredleme  15068  efgcpbllemb  15080  lt6abl  15197  ablfac1eu  15324  isrngd  15391  prdsrngd  15411  subrgsubg  15567  islmodd  15649  islssd  15709  islss4  15735  gzrngunit  16453  zrngunit  16454  prmirredlem  16462  expmhm  16465  znidomb  16531  isphld  16574  ocvocv  16587  ocvlss  16588  2ndcctbss  17197  isfild  17569  infil  17574  neifil  17591  flimfcls  17737  istgp2  17790  oppgtmd  17796  oppgtgp  17797  distgp  17798  indistgp  17799  symgtgp  17800  submtmd  17803  subgtgp  17804  divstgplem  17819  prdstmdd  17822  prdstgpd  17823  tlmtgp  17894  isngp4  18149  subgngp  18167  ngptgp  18168  tngngp2  18184  nrgtrg  18216  nrgtdrg  18219  elii2  18450  icopnfcnv  18456  xrhmeo  18460  lebnumii  18480  phtpcer  18509  reparpht  18512  phtpcco2  18513  pcohtpy  18534  pcoass  18538  pcorevlem  18540  pi1cpbl  18558  pi1grplem  18563  isclmi  18591  cphsubrglem  18629  cphclm  18641  tchclm  18678  tchcph  18683  clsocv  18693  pjthlem2  18818  ovolf  18857  iundisj2  18922  vitalilem2  18980  vitali  18984  itg2monolem3  19123  dvfsumlem1  19389  dvfsumlem3  19391  mon1puc1p  19552  uc1pmon1p  19553  ply1remlem  19564  drnguc1p  19572  plyaddlem1  19611  coeidlem  19635  aannenlem2  19725  radcnvcl  19809  pilem2  19844  coseq00topi  19886  coseq0negpitopi  19887  tangtx  19889  tanabsge  19890  cosq14gt0  19894  cosq14ge0  19895  cosordlem  19909  sinord  19912  resinf1o  19914  tanord1  19915  tanord  19916  efif1olem3  19922  relogrn  19935  logimclad  19946  logrnaddcl  19947  logneg  19957  logcj  19976  argregt0  19980  argrege0  19981  argimgt0  19982  argimlt0  19983  logimul  19984  logneg2  19985  logdmnrp  20004  logcnlem4  20008  dvloglem  20011  logf1o2  20013  efopnlem2  20020  cxpsqrlem  20065  asinneg  20198  asinsin  20204  acoscos  20205  acosbnd  20212  atancj  20222  atanlogaddlem  20225  atanlogsublem  20227  atanlogsub  20228  atantan  20235  atanbndlem  20237  atans2  20243  leibpi  20254  scvxcvx  20296  jensenlem2  20298  emcllem7  20311  basellem1  20334  ppisval  20357  chtdif  20412  ppidif  20417  ppiub  20459  chtublem  20466  chtub  20467  lgsdilem2  20586  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  2sqlem3  20621  chebbnd1lem1  20634  chebbnd1lem2  20635  chebbnd1lem3  20636  dchrisumlem2  20655  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  dchrisum0flblem2  20674  mulog2sumlem2  20700  logdivbnd  20721  pntpbnd2  20752  pntibndlem1  20754  pntibnd  20758  pntlemc  20760  pntlemg  20763  pntlemq  20766  pntlemf  20770  padicabvf  20796  padicabvcxp  20797  ostth2  20802  grpoinvf  20923  strlem3a  22848  hstrlem3a  22856  bcm1n  23048  ballotlemsel1i  23087  ballotlemfrceq  23103  xrge0iifcnv  23330  xrge0iifiso  23332  xrge0iifhom  23334  iundisj2fi  23379  iundisj2f  23381  esumc  23445  esumpinfsum  23460  erdszelem4  23740  erdszelem8  23744  txsconlem  23786  cvxscon  23789  cvmliftpht  23864  eupath2lem3  23918  snmlff  23927  sinccvglem  24020  axpaschlem  24640  areacirc  25034  cbcpcp  25265  inposet  25381  toplat  25393  trooo  25497  ltrooo  25507  rltrooo  25518  cntrset  25705  bsstrs  26249  nbssntrs  26250  bosser  26270  trer  26330  finlocfin  26402  locfindis  26408  locfincf  26409  nnubfi  26563  prter1  26850  nacsfix  26890  eldioph2lem1  26942  irrapxlem1  27010  rmxypairf1o  27099  jm2.27a  27201  frlmlbs  27352  hbtlem2  27431  hbt  27437  pmtrfconj  27510  psgnunilem2  27521  psgnunilem3  27522  psgnunilem4  27523  cntzsdrg  27613  hashgcdlem  27619  mon1pid  27627  mon1psubm  27628  fzossrbm1  28209  injresinjlem  28214  cyclnspth  28376  cyclispthon  28378  bnj944  29286  bnj998  29304  bnj1136  29343  bnj1408  29382  lkrlss  29907  diaf11N  31861  dibf11N  31973  lclkr  32345  lclkrs  32351  lcfrlem9  32362  lcfr  32397  mapd1o  32460  hdmapf1oN  32680  hgmapf1oN  32718
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator