Metamath Proof Explorer


Theorem bj-exlimd

Description: A slightly more general exlimd . A common usage will have ph substituted for ps and th substituted for ta , giving a form closer to exlimd . (Contributed by BJ, 25-Dec-2023)

Ref Expression
Hypotheses bj-exlimd.ph φ x ψ
bj-exlimd.th φ x θ τ
bj-exlimd.maj ψ χ θ
Assertion bj-exlimd φ x χ τ

Proof

Step Hyp Ref Expression
1 bj-exlimd.ph φ x ψ
2 bj-exlimd.th φ x θ τ
3 bj-exlimd.maj ψ χ θ
4 1 3 sylg φ x χ θ
5 bj-exlimg x θ τ x χ θ x χ τ
6 2 4 5 sylc φ x χ τ