3bitr4d - New Foundations Explorer

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

Theorem 3bitr4d 276

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)

**Hypotheses**
Ref	Expression
3bitr4d.1	⊢ (φ → (ψ ↔ χ))
3bitr4d.2	⊢ (φ → (θ ↔ ψ))
3bitr4d.3	⊢ (φ → (τ ↔ χ))

**Assertion**
Ref	Expression
3bitr4d	⊢ (φ → (θ ↔ τ))

**Proof of Theorem 3bitr4d**
Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 ⊢ (φ → (θ ↔ ψ))
2		3bitr4d.1	. . 3 ⊢ (φ → (ψ ↔ χ))
3		3bitr4d.3	. . 3 ⊢ (φ → (τ ↔ χ))
4	2, 3	bitr4d 247	. 2 ⊢ (φ → (ψ ↔ τ))
5	1, 4	bitrd 244	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: sbcom 2089 sbcom2 2114 r19.12sn 3789 lefinlteq 4463 eqtfinrelk 4486 tfinlefin 4502 opbrop 4841 fvopab3g 5386 unpreima 5408 inpreima 5409 respreima 5410 fconst5 5455 isotr 5495 ncseqnc 6128

W3C validator