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

Metamath Proof Explorer

Theorem exlimivv

Description: Inference form of Theorem 19.23 of Margaris p. 90, see 19.23 . (Contributed by NM, 1-Aug-1995)

		Ref	Expression
	Hypothesis	exlimivv.1	$⊢ φ \to ψ$
	Assertion	exlimivv	$⊢ \exists x \exists y φ \to ψ$

Step	Hyp	Ref	Expression
1		exlimivv.1	$⊢ φ \to ψ$
2	1	exlimiv	$⊢ \exists y φ \to ψ$
3	2	exlimiv	$⊢ \exists x \exists y φ \to ψ$