Metamath Proof Explorer


Theorem alrimdd

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

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

Proof

Step Hyp Ref Expression
1 alrimdd.1 xφ
2 alrimdd.2 φxψ
3 alrimdd.3 φψχ
4 2 nf5rd φψxψ
5 1 3 alimd φxψxχ
6 4 5 syld φψxχ