syl5rbb - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > syl5rbb		GIF version

Theorem syl5rbb 249

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 248	. 2 ⊢ (χ → (φ ↔ θ))
4	3	bicomd 192	1 ⊢ (χ → (θ ↔ φ))

Colors of variables: wff setvar class

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: syl5rbbr 251 csbabg 3197 uniiunlem 3353 opkelimagekg 4271 setswith 4321 fnresdisj 5193 f1oiso 5499