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

Theorem syl5rbbr 260
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl5rbbr.1
syl5rbbr.2
Assertion
Ref Expression
syl5rbbr

Proof of Theorem syl5rbbr
StepHypRef Expression
1 syl5rbbr.1 . . 3
21bicomi 202 . 2
3 syl5rbbr.2 . 2
42, 3syl5rbb 258 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  sbco3  2160  necon2bbid  2713  fressnfv  6085  eluniima  6162  dfac2  8532  alephval2  8968  adderpqlem  9353  1idpr  9428  leloe  9692  negeq0  9896  muleqadd  10218  addltmul  10799  xrleloe  11379  fzrev  11771  mod0  12003  modirr  12057  cjne0  12996  lenegsq  13153  fsumsplit  13562  sumsplit  13583  xpsfrnel  14960  isacs2  15050  acsfn  15056  comfeq  15101  sgrp2nmndlem3  16043  resscntz  16369  gexdvds  16604  hauscmplem  19906  hausdiag  20146  utop3cls  20754  ltgov  23983  colinearalglem2  24210  ax5seglem4  24235  mdsl2i  27241  addeq0  27558  pl1cn  27937  ghomfo  29031  ftc1anclem5  30094  fdc1  30239  stoweidlem28  31810  e2ebind  33336  lcvexchlem1  34759  lkreqN  34895  glbconxN  35102  islpln5  35259  islvol5  35303  cdlemefrs29bpre0  36122  cdlemg17h  36394  cdlemg33b  36433
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
  Copyright terms: Public domain W3C validator