Metamath Proof Explorer


Theorem bj-orim2

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

Ref Expression
Assertion bj-orim2 φ ψ χ φ χ ψ

Proof

Step Hyp Ref Expression
1 orc χ χ ψ
2 olc ψ χ ψ
3 2 imim2i φ ψ φ χ ψ
4 jao χ χ ψ φ χ ψ χ φ χ ψ
5 1 3 4 mpsyl φ ψ χ φ χ ψ