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 φψif-φθχif-ψθχ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wffφ
1 wps wffψ
2 0 1 wb wffφψ
3 wth wffθ
4 wch wffχ
5 0 3 4 wif wffif-φθχ
6 1 3 4 wif wffif-ψθχ
7 5 6 wi wffif-φθχif-ψθχ
8 2 7 wi wffφψif-φθχif-ψθχ