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

Metamath Proof Explorer

Theorem pm4.78

Description: Implication distributes over disjunction. Theorem *4.78 of WhiteheadRussell p. 121. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 19-Nov-2012)

Ref Expression
Assertion pm4.78 ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜑 → 𝜒 ) ) ↔ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 orordi ⊢ ( ( ¬ 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( ¬ 𝜑 ∨ 𝜒 ) ) )
2 imor ⊢ ( ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ↔ ( ¬ 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) )
3 imor ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 ∨ 𝜓 ) )
4 imor ⊢ ( ( 𝜑 → 𝜒 ) ↔ ( ¬ 𝜑 ∨ 𝜒 ) )
5 3 4 orbi12i ⊢ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜑 → 𝜒 ) ) ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( ¬ 𝜑 ∨ 𝜒 ) ) )
6 1 2 5 3bitr4ri ⊢ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜑 → 𝜒 ) ) ↔ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) )