Metamath Proof Explorer

Theorem exlimi

Description: Inference associated with 19.23 . See exlimiv for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016)

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


Step Hyp Ref Expression
1 exlimi.1 x ψ
2 exlimi.2 φ ψ
3 1 19.23 x φ ψ x φ ψ
4 3 2 mpgbi x φ ψ