Theorem exlimi

Description: Inference associated with 19.23 . See exlimiv for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016)

	Ref	Expression
Hypotheses	exlimi.1	|- F/ x ps
	exlimi.2	|- ( ph -> ps )
Assertion	exlimi	|- ( E. x ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		exlimi.1	|- F/ x ps
2		exlimi.2	|- ( ph -> ps )
3	1	19.23	|- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
4	3 2	mpgbi	|- ( E. x ph -> ps )