Theorem syl6rbb 196

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl6rbb

Step	Hyp	Ref	Expression
1		syl6rbb.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		syl6rbb.2	. . 3 |- ( ch <-> th )
3	1, 2	syl6bb 195	. 2 |- ( ph -> ( ps <-> th ) )
4	3	bicomd 140	1 |- ( ph -> ( th <-> ps ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl6rbbr  198  bibif  687  pm5.61  783  oranabs  804  pm5.7dc  938  nbbndc  1372  resopab2  4866  xpcom  5085  f1od2  6132  map1  6706  ac6sfi  6792  elznn0  9069  rexuz3  10762  xrmaxiflemcom  11018  metrest  12675  sincosq3sgn  12909  sincosq4sgn  12910