Theorem exlimii

Description: Inference associated with exlimi . Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		exlimii.1	|- F/ x ps
2		exlimii.2	|- ( ph -> ps )
3		exlimii.3	|- E. x ph
4	1 2	exlimi	|- ( E. x ph -> ps )
5	3 4	ax-mp	|- ps