Metamath Proof Explorer


Theorem eximii

Description: Inference associated with eximi . (Contributed by BJ, 3-Feb-2018)

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

Proof

Step Hyp Ref Expression
1 eximii.1 x φ
2 eximii.2 φ ψ
3 2 eximi x φ x ψ
4 1 3 ax-mp x ψ