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

Metamath Proof Explorer

Theorem albidv

Description: Formula-building rule for universal quantifier (deduction form). See also albidh and albid . (Contributed by NM, 26-May-1993)

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

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