Metamath Proof Explorer


Theorem alrimd

Description: Deduction form of Theorem 19.21 of Margaris p. 90, see 19.21 . (Contributed by Mario Carneiro, 24-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 alrimd.1 xφ
2 alrimd.2 xψ
3 alrimd.3 φψχ
4 2 a1i φxψ
5 1 4 3 alrimdd φψxχ