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  3516  fnressn  5290  fressnfv  5291  eluniimadm  5345  genpassl  6500  genpassu  6501  1idprl  6556  1idpru  6557  negeq0  7013  muleqadd  7383  crap0  7642  addltmul  7888  fzrev  8662  elabgf0  8850