Metamath Proof Explorer

Theorem pm4.42

Description: Theorem *4.42 of WhiteheadRussell p. 119. See also ifpid . (Contributed by Roy F. Longton, 21-Jun-2005)

Ref Expression
Assertion pm4.42 ⊢ φ ↔ φ ∧ ψ ∨ φ ∧ ¬ ψ

Proof

Step Hyp Ref Expression
1 dedlema ⊢ ψ → φ ↔ φ ∧ ψ ∨ φ ∧ ¬ ψ
2 dedlemb ⊢ ¬ ψ → φ ↔ φ ∧ ψ ∨ φ ∧ ¬ ψ
3 1 2 pm2.61i ⊢ φ ↔ φ ∧ ψ ∨ φ ∧ ¬ ψ