Metamath Proof Explorer


Theorem bj-currypeirce

Description: Curry's axiom curryax (a non-intuitionistic positive statement sometimes called a paradox of material implication) implies Peirce's axiom peirce over minimal implicational calculus and the axiomatic definition of disjunction (actually, only the elimination axiom jao via its inference form jaoi ; the introduction axioms olc and orc are not needed). Note that this theorem shows that actually, the standard instance of curryax implies the standard instance of peirce , which is not the case for the converse bj-peircecurry . (Contributed by BJ, 15-Jun-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-currypeirce
|- ( ( ph \/ ( ph -> ps ) ) -> ( ( ( ph -> ps ) -> ph ) -> ph ) )

Proof

Step Hyp Ref Expression
1 ax-1
 |-  ( ph -> ( ( ( ph -> ps ) -> ph ) -> ph ) )
2 pm2.27
 |-  ( ( ph -> ps ) -> ( ( ( ph -> ps ) -> ph ) -> ph ) )
3 1 2 jaoi
 |-  ( ( ph \/ ( ph -> ps ) ) -> ( ( ( ph -> ps ) -> ph ) -> ph ) )