Metamath Proof Explorer


Theorem exlimexi

Description: Inference similar to Theorem 19.23 of Margaris p. 90. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses exlimexi.1 ψ x ψ
exlimexi.2 x φ φ ψ
Assertion exlimexi x φ ψ

Proof

Step Hyp Ref Expression
1 exlimexi.1 ψ x ψ
2 exlimexi.2 x φ φ ψ
3 hbe1 x φ x x φ
4 3 1 2 exlimdh x φ x φ ψ
5 4 pm2.43i x φ ψ