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

Metamath Proof Explorer

Theorem alexbii

Description: Biconditional form of aleximi . (Contributed by BJ, 16-Nov-2020)

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

Step	Hyp	Ref	Expression
1		alexbii.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2	1	biimpd	$⊢ φ \to (ψ \to χ)$
3	2	aleximi	$⊢ \forall x φ \to (\exists x ψ \to \exists x χ)$
4	1	biimprd	$⊢ φ \to (χ \to ψ)$
5	4	aleximi	$⊢ \forall x φ \to (\exists x χ \to \exists x ψ)$
6	3 5	impbid	$⊢ \forall x φ \to (\exists x ψ \leftrightarrow \exists x χ)$