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

Metamath Proof Explorer

Theorem iotabidv

Description: Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011)

		Ref	Expression
	Hypothesis	iotabidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	iotabidv	$⊢ φ \to (ι x \| ψ) = (ι x \| χ)$

Step	Hyp	Ref	Expression
1		iotabidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2	1	alrimiv	$⊢ φ \to \forall x (ψ \leftrightarrow χ)$
3		iotabi	$⊢ \forall x (ψ \leftrightarrow χ) \to (ι x \| ψ) = (ι x \| χ)$
4	2 3	syl	$⊢ φ \to (ι x \| ψ) = (ι x \| χ)$