Metamath Proof Explorer


Theorem bj-sylget

Description: Dual statement of sylgt . Closed form of bj-sylge . (Contributed by BJ, 2-May-2019)

Ref Expression
Assertion bj-sylget x χ φ x φ ψ x χ ψ

Proof

Step Hyp Ref Expression
1 exim x χ φ x χ x φ
2 1 imim1d x χ φ x φ ψ x χ ψ