Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 2ralbidva.1 | ||
Assertion | 2ralbidva |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidva.1 | ||
2 | 1 | anassrs | |
3 | 2 | ralbidva | |
4 | 3 | ralbidva |