Metamath Proof Explorer


Axiom ax-frege1

Description: The case in which ph is denied, ps is affirmed, and ph is affirmed is excluded. This is evident since ph cannot at the same time be denied and affirmed. Axiom 1 of Frege1879 p. 26. Identical to ax-1 . (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

Ref Expression
Assertion ax-frege1 φ ψ φ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wff φ
1 wps wff ψ
2 1 0 wi wff ψ φ
3 0 2 wi wff φ ψ φ