Theorem syl5rbbr 184

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5rbbr

Step	Hyp	Ref	Expression
1		syl5rbbr.1	. . 3 ⊢ (ψ ↔ φ)
2	1	bicomi 123	. 2 ⊢ (φ ↔ ψ)
3		syl5rbbr.2	. 2 ⊢ (χ → (ψ ↔ θ))
4	2, 3	syl5rbb 182	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:  xordc  1280  sbal2  1895  eqsnm  3517  fnressn  5292  fressnfv  5293  eluniimadm  5347  genpassl  6507  genpassu  6508  1idprl  6566  1idpru  6567  negeq0  7061  muleqadd  7431  crap0  7691  addltmul  7938  fzrev  8716  cjap0  9135  cjne0  9136  elabgf0  9251