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	⊢ Ⅎ 𝑥 𝜓
	exlimii.2	⊢ ( 𝜑 → 𝜓 )
	exlimii.3	⊢ ∃ 𝑥 𝜑
Assertion	exlimii	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		exlimii.1	⊢ Ⅎ 𝑥 𝜓
2		exlimii.2	⊢ ( 𝜑 → 𝜓 )
3		exlimii.3	⊢ ∃ 𝑥 𝜑
4	1 2	exlimi	⊢ ( ∃ 𝑥 𝜑 → 𝜓 )
5	3 4	ax-mp	⊢ 𝜓