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

Metamath Proof Explorer

Theorem iotabii

Description: Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015)

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

Step	Hyp	Ref	Expression
1		iotabii.1	$⊢ φ \leftrightarrow ψ$
2		iotabi	$⊢ \forall x (φ \leftrightarrow ψ) \to (ι x \| φ) = (ι x \| ψ)$
3	2 1	mpg	$⊢ (ι x \| φ) = (ι x \| ψ)$