Theorem syl5bbr 250

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5bbr

Step	Hyp	Ref	Expression
1		syl5bbr.1	. . 3 ⊢ (ψ ↔ φ)
2	1	bicomi 193	. 2 ⊢ (φ ↔ ψ)
3		syl5bbr.2	. 2 ⊢ (χ → (ψ ↔ θ))
4	2, 3	syl5bb 248	1 ⊢ (χ → (φ ↔ θ))

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3bitr3g  278  biass  348  19.16  1860  19.19  1862  sbco2  2086  cbvab  2471  necon1bbid  2570  necon4abid  2580  elabgt  2982  sbceq1a  3056  sbcralt  3118  sbccsbg  3164  sbccsb2g  3165  opkelimagekg  4271  vfin1cltv  4547  phialllem1  4616  phiall  4618  xp11  5056  nfunv  5138  fnssresb  5195  fun11iun  5305  dffo4  5423  elunirn  5470  isomin  5496  resoprab2  5582  nchoicelem11  6299