Theorem syl5rbb 182

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

Hypotheses

Ref	Expression
syl5rbb.1	⊢ (φ ↔ ψ)
syl5rbb.2	⊢ (χ → (ψ ↔ θ))

Assertion

Ref	Expression
syl5rbb	⊢ (χ → (θ ↔ φ))

Proof of Theorem syl5rbb

Step	Hyp	Ref	Expression
1		syl5rbb.1	. . 3 ⊢ (φ ↔ ψ)
2		syl5rbb.2	. . 3 ⊢ (χ → (ψ ↔ θ))
3	1, 2	syl5bb 181	. 2 ⊢ (χ → (φ ↔ θ))
4	3	bicomd 129	1 ⊢ (χ → (θ ↔ φ))

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:  syl5rbbr  184  pm5.17dc  809  dn1dc  866  csbabg  2901  uniiunlem  3022  inimasn  4684  cnvpom  4803  fnresdisj  4952  f1oiso  5408  reldm  5754  1idprl  6566  1idpru  6567  nndiv  7735  fzn  8676  fz1sbc  8728  bj-indeq  9388