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  795  baib  828  pm5.6dc  835  xornbidc  1282  mo2dc  1955  reu8  2737  sbc6g  2788  r19.28m  3311  r19.45mv  3315  r19.27m  3316  ralsnsg  3407  ralsns  3408  rexsnsOLD  3410  iunconstm  3665  iinconstm  3666  unisucg  4151  funssres  4942  fncnv  4965  dff1o5  5135  funimass4  5224  fneqeql2  5276  fnniniseg2  5290  rexsupp  5291  unpreima  5292  dffo3  5314  funfvima  5390  dff13  5407  f1eqcocnv  5431  fliftf  5439  isocnv2  5452  eloprabga  5591  mpt22eqb  5610  opabex3d  5748  opabex3  5749  elxp6  5796  elxp7  5797  genpdflem  6605  ltnqpr  6691  ltexprlemloc  6705  xrlenlt  7084  negcon2  7264  elznn  8261  zq  8561  rpnegap  8615  shftdm  9423  rexanuz2  9589