Metamath Proof Explorer


Axiom ax-frege52a

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
|- ( ( ph <-> ps ) -> ( if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph
 |-  ph
1 wps
 |-  ps
2 0 1 wb
 |-  ( ph <-> ps )
3 wth
 |-  th
4 wch
 |-  ch
5 0 3 4 wif
 |-  if- ( ph , th , ch )
6 1 3 4 wif
 |-  if- ( ps , th , ch )
7 5 6 wi
 |-  ( if- ( ph , th , ch ) -> if- ( ps , th , ch ) )
8 2 7 wi
 |-  ( ( ph <-> ps ) -> ( if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )