Theorem syl5rbbr 275

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
syl5rbbr.1	|- ( ps <-> ph )
syl5rbbr.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5rbbr	|- ( ch -> ( th <-> ph ) )

Proof of Theorem syl5rbbr

Step	Hyp	Ref	Expression
1		syl5rbbr.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 214	. 2 |- ( ph <-> ps )
3		syl5rbbr.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	syl5rbb 273	1 |- ( ch -> ( th <-> ph ) )

Syntax hints:   -> wi 4   <-> wb 196

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

This theorem is referenced by:  sbco3  2417  necon2bbid  2837  fressnfv  6427  eluniima  6508  dfac2  8953  alephval2  9394  adderpqlem  9776  1idpr  9851  leloe  10124  negeq0  10335  muleqadd  10671  addltmul  11268  xrleloe  11977  fzrev  12403  mod0  12675  modirr  12741  cjne0  13903  lenegsq  14060  fsumsplit  14471  sumsplit  14499  dvdsabseq  15035  xpsfrnel  16223  isacs2  16314  acsfn  16320  comfeq  16366  sgrp2nmndlem3  17412  resscntz  17764  gexdvds  17999  hauscmplem  21209  hausdiag  21448  utop3cls  22055  ltgov  25492  ax5seglem4  25812  mdsl2i  29181  addeq0  29510  pl1cn  30001  topdifinfeq  33198  finxpreclem6  33233  ftc1anclem5  33489  fdc1  33542  relcnveq  34093  relcnveq2  34094  lcvexchlem1  34321  lkreqN  34457  glbconxN  34664  islpln5  34821  islvol5  34865  cdlemefrs29bpre0  35684  cdlemg17h  35956  cdlemg33b  35995  brnonrel  37895  frege92  38249  e2ebind  38779  stoweidlem28  40245