Metamath Proof Explorer


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 ψ
exlimii.2 φ ψ
exlimii.3 x φ
Assertion exlimii ψ

Proof

Step Hyp Ref Expression
1 exlimii.1 x ψ
2 exlimii.2 φ ψ
3 exlimii.3 x φ
4 1 2 exlimi x φ ψ
5 3 4 ax-mp ψ