Theorem syl5rbbr 193

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 130	. 2 |- ( ph <-> ps )
3		syl5rbbr.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	syl5rbb 191	1 |- ( ch -> ( th <-> ph ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  xordc  1324  sbal2  1940  eqsnm  3555  fnressn  5381  fressnfv  5382  eluniimadm  5436  genpassl  6776  genpassu  6777  1idprl  6842  1idpru  6843  axcaucvglemres  7127  negeq0  7429  muleqadd  7825  crap0  8102  addltmul  8334  fzrev  9177  modq0  9411  cjap0  9932  cjne0  9933  caucvgrelemrec  10003  lenegsq  10119  dvdsabseq  10392  oddennn  10730  elabgf0  10765