This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem anbi1i

Description: Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 16-Nov-2013)

		Ref	Expression
	Hypothesis	anbi.1	$⊢ φ \leftrightarrow ψ$
	Assertion	anbi1i	$⊢ (φ \land χ) \leftrightarrow (ψ \land χ)$

Proof

Step	Hyp	Ref	Expression
1		anbi.1	$⊢ φ \leftrightarrow ψ$
2	1	a1i	$⊢ χ \to (φ \leftrightarrow ψ)$
3	2	pm5.32ri	$⊢ (φ \land χ) \leftrightarrow (ψ \land χ)$