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

Metamath Proof Explorer

Theorem 19.23bi

Description: Inference form of Theorem 19.23 of Margaris p. 90, see 19.23 . (Contributed by NM, 12-Mar-1993)

		Ref	Expression
	Hypothesis	19.23bi.1	$⊢ \exists x φ \to ψ$
	Assertion	19.23bi	$⊢ φ \to ψ$

Step	Hyp	Ref	Expression
1		19.23bi.1	$⊢ \exists x φ \to ψ$
2		19.8a	$⊢ φ \to \exists x φ$
3	2 1	syl	$⊢ φ \to ψ$