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

Metamath Proof Explorer

Theorem exbidv

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh and exbid . (Contributed by NM, 26-May-1993)

		Ref	Expression
	Hypothesis	albidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	exbidv	$⊢ φ \to (\exists x ψ \leftrightarrow \exists x χ)$

Step	Hyp	Ref	Expression
1		albidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		ax-5	$⊢ φ \to \forall x φ$
3	2 1	exbidh	$⊢ φ \to (\exists x ψ \leftrightarrow \exists x χ)$