Description: Lemma for frege102 (via frege92 ). Proposition 53 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | frege53b | |- ( [ y / x ] ph -> ( y = z -> [ z / x ] ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frege52b | |- ( y = z -> ( [ y / x ] ph -> [ z / x ] ph ) ) |
|
| 2 | ax-frege8 | |- ( ( y = z -> ( [ y / x ] ph -> [ z / x ] ph ) ) -> ( [ y / x ] ph -> ( y = z -> [ z / x ] ph ) ) ) |
|
| 3 | 1 2 | ax-mp | |- ( [ y / x ] ph -> ( y = z -> [ z / x ] ph ) ) |