Theorem syl5rbbr 194

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  xordc  1329  sbal2  1947  eqsnm  3607  fnressn  5499  fressnfv  5500  eluniimadm  5560  genpassl  7146  genpassu  7147  1idprl  7212  1idpru  7213  axcaucvglemres  7497  negeq0  7799  muleqadd  8200  crap0  8481  addltmul  8715  fzrev  9561  modq0  9799  cjap0  10404  cjne0  10405  caucvgrelemrec  10475  lenegsq  10591  isumss  10846  fsumsplit  10864  sumsplitdc  10889  dvdsabseq  11189  oddennn  11546  elabgf0  11981