Metamath Proof Explorer

Theorem pm4.39

Description: Theorem *4.39 of WhiteheadRussell p. 118. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm4.39 ⊢φ↔χ∧ψ↔θ→φ∨ψ↔χ∨θ

Proof

Step Hyp Ref Expression
1 simpl ⊢φ↔χ∧ψ↔θ→φ↔χ
2 simpr ⊢φ↔χ∧ψ↔θ→ψ↔θ
3 1 2 orbi12d ⊢φ↔χ∧ψ↔θ→φ∨ψ↔χ∨θ