Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | gen2.1 | |- ph |
|
| Assertion | gen2 | |- A. x A. y ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | gen2.1 | |- ph |
|
| 2 | 1 | ax-gen | |- A. y ph |
| 3 | 2 | ax-gen | |- A. x A. y ph |