Description: Restricted quantifier version of Theorem 19.40 of Margaris p. 90. (Contributed by NM, 2-Apr-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | r19.40 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | 1 | reximi | |
3 | simpr | |
|
4 | 3 | reximi | |
5 | 2 4 | jca | |