Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-frege52a Structured version   Visualization version   GIF version

Axiom ax-frege52a 40081
Description: The case when the content of 𝜑 is identical with the content of 𝜓 and in which a proposition controlled by an element for which we substitute the content of 𝜑 is affirmed (in this specific case the identity logical function) and the same proposition, this time where we substituted the content of 𝜓, is denied does not take place. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
Assertion
Ref Expression
ax-frege52a ((𝜑𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒)))

Detailed syntax breakdown of Axiom ax-frege52a
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wb 207 . 2 wff (𝜑𝜓)
4 wth . . . 4 wff 𝜃
5 wch . . . 4 wff 𝜒
61, 4, 5wif 1054 . . 3 wff if-(𝜑, 𝜃, 𝜒)
72, 4, 5wif 1054 . . 3 wff if-(𝜓, 𝜃, 𝜒)
86, 7wi 4 . 2 wff (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))
93, 8wi 4 1 wff ((𝜑𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  frege52aid  40082  frege53a  40084  frege57a  40097
  Copyright terms: Public domain W3C validator