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

Metamath Proof Explorer

Theorem pm5.62

Description: Theorem *5.62 of WhiteheadRussell p. 125. (Contributed by Roy F. Longton, 21-Jun-2005)

Ref Expression
Assertion pm5.62 ⊢ φ ∧ ψ ∨ ¬ ψ ↔ φ ∨ ¬ ψ

Proof

Step Hyp Ref Expression
1 exmid ⊢ ψ ∨ ¬ ψ
2 ordir ⊢ φ ∧ ψ ∨ ¬ ψ ↔ φ ∨ ¬ ψ ∧ ψ ∨ ¬ ψ
3 1 2 mpbiran2 ⊢ φ ∧ ψ ∨ ¬ ψ ↔ φ ∨ ¬ ψ