Metamath Proof Explorer


Theorem alrimdh

Description: Deduction form of Theorem 19.21 of Margaris p. 90, see 19.21 and 19.21h . (Contributed by NM, 10-Feb-1997) (Proof shortened by Andrew Salmon, 13-May-2011)

Ref Expression
Hypotheses alrimdh.1 φ x φ
alrimdh.2 ψ x ψ
alrimdh.3 φ ψ χ
Assertion alrimdh φ ψ x χ

Proof

Step Hyp Ref Expression
1 alrimdh.1 φ x φ
2 alrimdh.2 ψ x ψ
3 alrimdh.3 φ ψ χ
4 1 3 alimdh φ x ψ x χ
5 2 4 syl5 φ ψ x χ