Metamath Proof Explorer


Theorem bj-sylge

Description: Dual statement of sylg (the final "e" in the label stands for "existential (version of sylg )". Variant of exlimih . (Contributed by BJ, 25-Dec-2023)

Ref Expression
Hypotheses bj-sylge.nf x φ ψ
bj-sylge.maj χ φ
Assertion bj-sylge x χ ψ

Proof

Step Hyp Ref Expression
1 bj-sylge.nf x φ ψ
2 bj-sylge.maj χ φ
3 2 eximi x χ x φ
4 3 1 syl x χ ψ