Metamath Proof Explorer


Theorem bj-sylget2

Description: Uncurried (imported) form of bj-sylget . (Contributed by BJ, 2-May-2019)

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

Proof

Step Hyp Ref Expression
1 bj-sylget x φ ψ x ψ χ x φ χ
2 1 imp x φ ψ x ψ χ x φ χ