Metamath Proof Explorer


Theorem 3orcoma

Description: Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Assertion 3orcoma φ ψ χ ψ φ χ

Proof

Step Hyp Ref Expression
1 or12 φ ψ χ ψ φ χ
2 3orass φ ψ χ φ ψ χ
3 3orass ψ φ χ ψ φ χ
4 1 2 3 3bitr4i φ ψ χ ψ φ χ