Description: Theorem 19.32 of Margaris p. 90. See 19.32v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 24-Sep-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | 19.32.1 | |- F/ x ph |
|
| Assertion | 19.32 | |- ( A. x ( ph \/ ps ) <-> ( ph \/ A. x ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.32.1 | |- F/ x ph |
|
| 2 | 1 | nfn | |- F/ x -. ph |
| 3 | 2 | 19.21 | |- ( A. x ( -. ph -> ps ) <-> ( -. ph -> A. x ps ) ) |
| 4 | df-or | |- ( ( ph \/ ps ) <-> ( -. ph -> ps ) ) |
|
| 5 | 4 | albii | |- ( A. x ( ph \/ ps ) <-> A. x ( -. ph -> ps ) ) |
| 6 | df-or | |- ( ( ph \/ A. x ps ) <-> ( -. ph -> A. x ps ) ) |
|
| 7 | 3 5 6 | 3bitr4i | |- ( A. x ( ph \/ ps ) <-> ( ph \/ A. x ps ) ) |