Description: The case when the content of ph is identical with the content of ps and in which a proposition controlled by an element for which we substitute the content of ph is affirmed (in this specific case the identity logical function) and the same proposition, this time where we substituted the content of ps , is denied does not take place. Part of Axiom 52 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-frege52a | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( if- ( 𝜑 , 𝜃 , 𝜒 ) → if- ( 𝜓 , 𝜃 , 𝜒 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | wph | ⊢ 𝜑 | |
| 1 | wps | ⊢ 𝜓 | |
| 2 | 0 1 | wb | ⊢ ( 𝜑 ↔ 𝜓 ) |
| 3 | wth | ⊢ 𝜃 | |
| 4 | wch | ⊢ 𝜒 | |
| 5 | 0 3 4 | wif | ⊢ if- ( 𝜑 , 𝜃 , 𝜒 ) |
| 6 | 1 3 4 | wif | ⊢ if- ( 𝜓 , 𝜃 , 𝜒 ) |
| 7 | 5 6 | wi | ⊢ ( if- ( 𝜑 , 𝜃 , 𝜒 ) → if- ( 𝜓 , 𝜃 , 𝜒 ) ) |
| 8 | 2 7 | wi | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( if- ( 𝜑 , 𝜃 , 𝜒 ) → if- ( 𝜓 , 𝜃 , 𝜒 ) ) ) |