Metamath Proof Explorer


Theorem orcomd

Description: Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010)

Ref Expression
Hypothesis orcomd.1 φ ψ χ
Assertion orcomd φ χ ψ

Proof

Step Hyp Ref Expression
1 orcomd.1 φ ψ χ
2 orcom ψ χ χ ψ
3 1 2 sylib φ χ ψ