Theorem syl6rbbr 255

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

Hypotheses

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

Assertion

Ref	Expression
syl6rbbr	|- (ph -> (th <-> ps))

Proof of Theorem syl6rbbr

Step	Hyp	Ref	Expression
1		syl6rbbr.1	. 2 |- (ph -> (ps <-> ch))
2		syl6rbbr.2	. . 3 |- (th <-> ch)
3	2	bicomi 193	. 2 |- (ch <-> th)
4	1, 3	syl6rbb 253	1 |- (ph -> (th <-> ps))

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

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

This theorem is referenced by:  baib  871  reu8  3032  sbc6g  3071  r19.28z  3642  r19.28zv  3645  r19.37zv  3646  r19.45zv  3647  r19.27z  3648  r19.27zv  3649  r19.36zv  3650  ralidm  3653  ralsns  3763  rexsns  3764  ssunsn2  3865  iunconst  3977  iinconst  3978  ssofss  4076  snelpwg  4114  opres  4978  cores  5084  funssres  5144  fncnv  5158  dff1o5  5295  fvres  5342  funimass4  5368  dffo3  5422  funfvima  5459  eloprabga  5578  eqncg  6126  ncseqnc  6128  eqtc  6161  tcfnex  6244  nchoicelem11  6299  nchoicelem16  6304  nchoicelem18  6306  canncb  6332