This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orcom

Description: Commutative law for disjunction. Theorem *4.31 of WhiteheadRussell p. 118. (Contributed by NM, 3-Jan-1993) (Proof shortened by Wolf Lammen, 15-Nov-2012)

Ref Expression
Assertion orcom ⊢ φ ∨ ψ ↔ ψ ∨ φ

Proof

Step Hyp Ref Expression
1 pm1.4 ⊢ φ ∨ ψ → ψ ∨ φ
2 pm1.4 ⊢ ψ ∨ φ → φ ∨ ψ
3 1 2 impbii ⊢ φ ∨ ψ ↔ ψ ∨ φ