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

Metamath Proof Explorer

Theorem pm4.79

Description: Theorem *4.79 of WhiteheadRussell p. 121. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 27-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 id ⊢ ( ( 𝜓 → 𝜑 ) → ( 𝜓 → 𝜑 ) )
2 id ⊢ ( ( 𝜒 → 𝜑 ) → ( 𝜒 → 𝜑 ) )
3 1 2 jaoa ⊢ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜑 ) ) → ( ( 𝜓 ∧ 𝜒 ) → 𝜑 ) )
4 simplim ⊢ ( ¬ ( 𝜓 → 𝜑 ) → 𝜓 )
5 pm3.3 ⊢ ( ( ( 𝜓 ∧ 𝜒 ) → 𝜑 ) → ( 𝜓 → ( 𝜒 → 𝜑 ) ) )
6 4 5 syl5 ⊢ ( ( ( 𝜓 ∧ 𝜒 ) → 𝜑 ) → ( ¬ ( 𝜓 → 𝜑 ) → ( 𝜒 → 𝜑 ) ) )
7 6 orrd ⊢ ( ( ( 𝜓 ∧ 𝜒 ) → 𝜑 ) → ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜑 ) ) )
8 3 7 impbii ⊢ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜑 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) → 𝜑 ) )