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	$⊢ (φ \lor (φ \to ψ))$

Proof

Step	Hyp	Ref	Expression
1		orc	$⊢ φ \to (φ \lor (φ \to ψ))$
2		olc	$⊢ (φ \to ψ) \to (φ \lor (φ \to ψ))$
3		peirce	$⊢ (((φ \lor (φ \to ψ)) \to φ) \to (φ \lor (φ \to ψ))) \to (φ \lor (φ \to ψ))$
4		peirce	$⊢ ((φ \to ψ) \to φ) \to φ$
5		peirceroll	$⊢ (((φ \to ψ) \to φ) \to φ) \to (((φ \to ψ) \to (φ \lor (φ \to ψ))) \to (((φ \lor (φ \to ψ)) \to φ) \to φ))$
6	4 5	ax-mp	$⊢ ((φ \to ψ) \to (φ \lor (φ \to ψ))) \to (((φ \lor (φ \to ψ)) \to φ) \to φ)$
7		peirceroll	$⊢ ((((φ \lor (φ \to ψ)) \to φ) \to (φ \lor (φ \to ψ))) \to (φ \lor (φ \to ψ))) \to ((((φ \lor (φ \to ψ)) \to φ) \to φ) \to ((φ \to (φ \lor (φ \to ψ))) \to (φ \lor (φ \to ψ))))$
8	3 6 7	mpsyl	$⊢ ((φ \to ψ) \to (φ \lor (φ \to ψ))) \to ((φ \to (φ \lor (φ \to ψ))) \to (φ \lor (φ \to ψ)))$
9	2 8	ax-mp	$⊢ (φ \to (φ \lor (φ \to ψ))) \to (φ \lor (φ \to ψ))$
10	1 9	ax-mp	$⊢ (φ \lor (φ \to ψ))$

Metamath Proof Explorer

Theorem bj-peircecurry

Proof