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	$$⊢Ⅎx\psi$$
	exlimii.2	$$⊢\phi \to \psi$$
	exlimii.3	$$⊢\exists x\phi$$
Assertion	exlimii	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		exlimii.1	$$⊢Ⅎx\psi$$
2		exlimii.2	$$⊢\phi \to \psi$$
3		exlimii.3	$$⊢\exists x\phi$$
4	1 2	exlimi	$$⊢\exists x\phi \to \psi$$
5	3 4	ax-mp	$$⊢\psi$$