Metamath Proof Explorer


Theorem bj-alrimd

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

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

Proof

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