Description: Proof of orim2 from the axiomatic definition of disjunction ( olc , orc , jao ) and minimal implicational calculus. (Contributed by BJ, 4-Apr-2021) (Proof modification is discouraged.)