Theorem syl5rbb 191

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

Hypotheses

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

Assertion

Ref	Expression
syl5rbb	|- ( ch -> ( th <-> ph ) )

Proof of Theorem syl5rbb

Step	Hyp	Ref	Expression
1		syl5rbb.1	. . 3 |- ( ph <-> ps )
2		syl5rbb.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	syl5bb 190	. 2 |- ( ch -> ( ph <-> th ) )
4	3	bicomd 139	1 |- ( ch -> ( th <-> ph ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl5rbbr  193  pm5.17dc  843  dn1dc  901  csbabg  2963  uniiunlem  3082  inimasn  4761  cnvpom  4880  fnresdisj  5029  f1oiso  5485  reldm  5832  1idprl  6780  1idpru  6781  nndiv  8079  fzn  9061  fz1sbc  9113  bj-indeq  10724