Theorem syl6rbbr 188

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 123	. 2 |- (ch <-> th)
4	1, 3	syl6rbb 186	1 |- (ph -> (th <-> ps))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  imimorbdc  794  baib  827  pm5.6dc  834  xornbidc  1279  mo2dc  1952  reu8  2731  sbc6g  2782  r19.28m  3305  r19.45mv  3309  r19.27m  3310  ralsns  3399  rexsnsOLD  3401  iunconstm  3656  iinconstm  3657  unisucg  4117  funssres  4885  fncnv  4908  dff1o5  5078  funimass4  5167  fneqeql2  5219  fnniniseg2  5233  rexsupp  5234  unpreima  5235  dffo3  5257  funfvima  5333  dff13  5350  f1eqcocnv  5374  fliftf  5382  isocnv2  5395  eloprabga  5533  mpt22eqb  5552  opabex3d  5690  opabex3  5691  elxp6  5738  elxp7  5739  genpdflem  6490  ltexprlemloc  6581  xrlenlt  6881  negcon2  7060  elznn  8037  zq  8337  rpnegap  8390