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  4643  soisores  5824  onfununi  6358  smores2  6371  smoiso  6379  oelimcl  6598  iserd  6686  erinxp  6733  resixp  6851  undifixp  6852  alephval3  7737  fpwwe2lem12  8263  canthwelem  8272  canthwe  8273  r1limwun  8358  wunex2  8360  tskcard  8403  gruina  8440  nqerf  8554  nqerid  8557  uztrn  10244  zsupss  10307  xov1plusxeqvd  10780  elfzolt2b  10885  elfzolt3b  10886  elfzouz2  10888  elfzo0  10904  fzostep1  10922  flword2  10943  uzsup  10967  fzsdom2  11382  ccatval1  11431  wrdeqs1cat  11475  swrds2  11560  rexuzre  11836  limsupgre  11955  rlimclim1  12019  rlimclim  12020  climrlim2  12021  isercolllem1  12138  isercoll  12141  climcndslem1  12308  tanhbnd  12441  sinbnd2  12462  cosbnd2  12463  rpnnen2  12504  bitsfzolem  12625  bitsfzo  12626  bitsmod  12627  bitsfi  12628  bitsinv1lem  12632  bitsinv1  12633  smueqlem  12681  zgz  12980  gznegcl  12982  gzcjcl  12983  gzaddcl  12984  gzmulcl  12985  vdwlem9  13036  ismred  13504  isfuncd  13739  homdmcoa  13899  isdrs2  14073  fpwipodrs  14267  ipodrsima  14268  psss  14323  psssdm2  14324  subgid  14623  issubg2  14636  subsubg  14640  gaorber  14762  orbsta  14767  pgpfi1  14906  subgpgp  14908  pgpssslw  14925  subgslw  14927  sylow2alem2  14929  fislw  14936  sylow3lem3  14940  efgs1  15044  efgsp1  15046  efgsres  15047  efgredleme  15052  efgcpbllemb  15064  lt6abl  15181  ablfac1eu  15308  isrngd  15375  prdsrngd  15395  subrgsubg  15551  islmodd  15633  islssd  15693  islss4  15719  gzrngunit  16437  zrngunit  16438  prmirredlem  16446  expmhm  16449  znidomb  16515  isphld  16558  ocvocv  16571  ocvlss  16572  2ndcctbss  17181  isfild  17553  infil  17558  neifil  17575  flimfcls  17721  istgp2  17774  oppgtmd  17780  oppgtgp  17781  distgp  17782  indistgp  17783  symgtgp  17784  submtmd  17787  subgtgp  17788  divstgplem  17803  prdstmdd  17806  prdstgpd  17807  tlmtgp  17878  isngp4  18133  subgngp  18151  ngptgp  18152  tngngp2  18168  nrgtrg  18200  nrgtdrg  18203  elii2  18434  icopnfcnv  18440  xrhmeo  18444  lebnumii  18464  phtpcer  18493  reparpht  18496  phtpcco2  18497  pcohtpy  18518  pcoass  18522  pcorevlem  18524  pi1cpbl  18542  pi1grplem  18547  isclmi  18575  cphsubrglem  18613  cphclm  18625  tchclm  18662  tchcph  18667  clsocv  18677  pjthlem2  18802  ovolf  18841  iundisj2  18906  vitalilem2  18964  vitali  18968  itg2monolem3  19107  dvfsumlem1  19373  dvfsumlem3  19375  mon1puc1p  19536  uc1pmon1p  19537  ply1remlem  19548  drnguc1p  19556  plyaddlem1  19595  coeidlem  19619  aannenlem2  19709  radcnvcl  19793  pilem2  19828  coseq00topi  19870  coseq0negpitopi  19871  tangtx  19873  tanabsge  19874  cosq14gt0  19878  cosq14ge0  19879  cosordlem  19893  sinord  19896  resinf1o  19898  tanord1  19899  tanord  19900  efif1olem3  19906  relogrn  19919  logimclad  19930  logrnaddcl  19931  logneg  19941  logcj  19960  argregt0  19964  argrege0  19965  argimgt0  19966  argimlt0  19967  logimul  19968  logneg2  19969  logdmnrp  19988  logcnlem4  19992  dvloglem  19995  logf1o2  19997  efopnlem2  20004  cxpsqrlem  20049  asinneg  20182  asinsin  20188  acoscos  20189  acosbnd  20196  atancj  20206  atanlogaddlem  20209  atanlogsublem  20211  atanlogsub  20212  atantan  20219  atanbndlem  20221  atans2  20227  leibpi  20238  scvxcvx  20280  jensenlem2  20282  emcllem7  20295  basellem1  20318  ppisval  20341  chtdif  20396  ppidif  20401  ppiub  20443  chtublem  20450  chtub  20451  lgsdilem2  20570  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  2sqlem3  20605  chebbnd1lem1  20618  chebbnd1lem2  20619  chebbnd1lem3  20620  dchrisumlem2  20639  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  dchrisum0flblem2  20658  mulog2sumlem2  20684  logdivbnd  20705  pntpbnd2  20736  pntibndlem1  20738  pntibnd  20742  pntlemc  20744  pntlemg  20747  pntlemq  20750  pntlemf  20754  padicabvf  20780  padicabvcxp  20781  ostth2  20786  grpoinvf  20907  strlem3a  22832  hstrlem3a  22840  bcm1n  23032  ballotlemsel1i  23071  ballotlemfrceq  23087  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  iundisj2fi  23364  iundisj2f  23366  esumc  23430  esumpinfsum  23445  erdszelem4  23725  erdszelem8  23729  txsconlem  23771  cvxscon  23774  cvmliftpht  23849  eupath2lem3  23903  snmlff  23912  sinccvglem  24005  axpaschlem  24568  areacirc  24931  cbcpcp  25162  inposet  25278  toplat  25290  trooo  25394  ltrooo  25404  rltrooo  25415  cntrset  25602  bsstrs  26146  nbssntrs  26147  bosser  26167  trer  26227  finlocfin  26299  locfindis  26305  locfincf  26306  nnubfi  26460  prter1  26747  nacsfix  26787  eldioph2lem1  26839  irrapxlem1  26907  rmxypairf1o  26996  jm2.27a  27098  frlmlbs  27249  hbtlem2  27328  hbt  27334  pmtrfconj  27407  psgnunilem2  27418  psgnunilem3  27419  psgnunilem4  27420  cntzsdrg  27510  hashgcdlem  27516  mon1pid  27524  mon1psubm  27525  bnj944  28970  bnj998  28988  bnj1136  29027  bnj1408  29066  lkrlss  29285  diaf11N  31239  dibf11N  31351  lclkr  31723  lclkrs  31729  lcfrlem9  31740  lcfr  31775  mapd1o  31838  hdmapf1oN  32058  hgmapf1oN  32096
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