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

Metamath Proof Explorer

Theorem cases2

Description: Case disjunction according to the value of ph . (Contributed by BJ, 6-Apr-2019) (Proof shortened by Wolf Lammen, 28-Feb-2022)

Ref Expression
Assertion cases2 ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 pm4.83 ⊢ ( ( ( 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) ∧ ( ¬ 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) ) ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) )
2 dedlema ⊢ ( 𝜑 → ( 𝜓 ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )
3 2 pm5.74i ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )
4 dedlemb ⊢ ( ¬ 𝜑 → ( 𝜒 ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )
5 4 pm5.74i ⊢ ( ( ¬ 𝜑 → 𝜒 ) ↔ ( ¬ 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )
6 3 5 anbi12i ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ↔ ( ( 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) ∧ ( ¬ 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) ) )
7 ancom ⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝜑 ) )
8 ancom ⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) ↔ ( 𝜒 ∧ ¬ 𝜑 ) )
9 7 8 orbi12i ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) )
10 1 6 9 3bitr4ri ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )