Description: Deduction quantifying both antecedent and consequent. (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ralimda.1 | ||
ralimda.2 | |||
Assertion | ralimda |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimda.1 | ||
2 | ralimda.2 | ||
3 | nfra1 | ||
4 | 1 3 | nfan | |
5 | id | ||
6 | 5 | adantlr | |
7 | rspa | ||
8 | 7 | adantll | |
9 | 6 8 2 | sylc | |
10 | 4 9 | ralrimia | |
11 | 10 | ex |