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.)