Description: Theorem 19.16 of Margaris p. 90. (Contributed by NM, 12-Mar-1993)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | 19.16.1 | |- F/ x ph |
|
| Assertion | 19.16 | |- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.16.1 | |- F/ x ph |
|
| 2 | 1 | 19.3 | |- ( A. x ph <-> ph ) |
| 3 | albi | |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) ) |
|
| 4 | 2 3 | bitr3id | |- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) ) |