Metamath Proof Explorer


Theorem bj-sylgt2

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

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

Proof

Step Hyp Ref Expression
1 sylgt x ψ χ φ x ψ φ x χ
2 1 imp x ψ χ φ x ψ φ x χ