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-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  baib  871  reu8  3033  sbc6g  3072  r19.28z  3643  r19.28zv  3646  r19.37zv  3647  r19.45zv  3648  r19.27z  3649  r19.27zv  3650  r19.36zv  3651  ralidm  3654  ralsns  3764  rexsns  3765  ssunsn2  3866  iunconst  3978  iinconst  3979  ssofss  4077  snelpwg  4115  opres  4979  cores  5085  funssres  5145  fncnv  5159  dff1o5  5296  fvres  5343  funimass4  5369  dffo3  5423  funfvima  5460  eloprabga  5579  eqncg  6127  ncseqnc  6129  eqtc  6162  tcfnex  6245  nchoicelem11  6300  nchoicelem16  6305  nchoicelem18  6307  canncb  6333