3anbi1d - New Foundations Explorer

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

Theorem 3anbi1d 1256

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

**Hypothesis**
Ref	Expression
3anbi1d.1	⊢ (φ → (ψ ↔ χ))

**Assertion**
Ref	Expression
3anbi1d	⊢ (φ → ((ψ ∧ θ ∧ τ) ↔ (χ ∧ θ ∧ τ)))

**Proof of Theorem 3anbi1d**
Step	Hyp	Ref	Expression
1		3anbi1d.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		biidd 228	. 2 ⊢ (φ → (θ ↔ θ))
3	1, 2	3anbi12d 1253	1 ⊢ (φ → ((ψ ∧ θ ∧ τ) ↔ (χ ∧ θ ∧ τ)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 176 ∧ w3a 934

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 df-an 360 df-3an 936

This theorem is referenced by: vtocl3gaf 2923 opkelins2kg 4251 opkelins3kg 4252 opkelsikg 4264 sikss1c1c 4267 brsi 4761 funsi 5520 brsnsi 5773 fnpprod 5843 ovce 6172