Metamath Proof Explorer

Theorem bj-peircecurry

Description: Peirce's axiom peirce implies Curry's axiom curryax over minimal implicational calculus and the axiomatic definition of disjunction (actually, only the introduction axioms olc and orc ; the elimination axiom jao is not needed). See bj-currypeirce for the converse. (Contributed by BJ, 15-Jun-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( ph -> ( ph \/ ( ph -> ps ) ) )
2 olc 
 |-  ( ( ph -> ps ) -> ( ph \/ ( ph -> ps ) ) )
3 peirce 
 |-  ( ( ( ( ph \/ ( ph -> ps ) ) -> ph ) -> ( ph \/ ( ph -> ps ) ) ) -> ( ph \/ ( ph -> ps ) ) )
4 peirce 
 |-  ( ( ( ph -> ps ) -> ph ) -> ph )
5 peirceroll 
 |-  ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ph -> ps ) -> ( ph \/ ( ph -> ps ) ) ) -> ( ( ( ph \/ ( ph -> ps ) ) -> ph ) -> ph ) ) )
6 4 5 ax-mp 
 |-  ( ( ( ph -> ps ) -> ( ph \/ ( ph -> ps ) ) ) -> ( ( ( ph \/ ( ph -> ps ) ) -> ph ) -> ph ) )
7 peirceroll 
 |-  ( ( ( ( ( ph \/ ( ph -> ps ) ) -> ph ) -> ( ph \/ ( ph -> ps ) ) ) -> ( ph \/ ( ph -> ps ) ) ) -> ( ( ( ( ph \/ ( ph -> ps ) ) -> ph ) -> ph ) -> ( ( ph -> ( ph \/ ( ph -> ps ) ) ) -> ( ph \/ ( ph -> ps ) ) ) ) )
8 3 6 7 mpsyl 
 |-  ( ( ( ph -> ps ) -> ( ph \/ ( ph -> ps ) ) ) -> ( ( ph -> ( ph \/ ( ph -> ps ) ) ) -> ( ph \/ ( ph -> ps ) ) ) )
9 2 8 ax-mp 
 |-  ( ( ph -> ( ph \/ ( ph -> ps ) ) ) -> ( ph \/ ( ph -> ps ) ) )
10 1 9 ax-mp 
 |-  ( ph \/ ( ph -> ps ) )