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 | |
|
alrimdd.2 | |
||
alrimdd.3 | |
||
Assertion | alrimdd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimdd.1 | |
|
2 | alrimdd.2 | |
|
3 | alrimdd.3 | |
|
4 | 2 | nf5rd | |
5 | 1 3 | alimd | |
6 | 4 5 | syld | |