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

Metamath Proof Explorer

Theorem cases2ALT

Description: Alternate proof of cases2 , not using dedlema or dedlemb . (Contributed by BJ, 6-Apr-2019) (Proof shortened by Wolf Lammen, 2-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pm3.4 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) )
2 pm2.24 ⊢ ( 𝜑 → ( ¬ 𝜑 → 𝜒 ) )
3 2 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ¬ 𝜑 → 𝜒 ) )
4 1 3 jca ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )
5 pm2.21 ⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
6 5 adantr ⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → ( 𝜑 → 𝜓 ) )
7 pm3.4 ⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → ( ¬ 𝜑 → 𝜒 ) )
8 6 7 jca ⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )
9 4 8 jaoi ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )
10 pm2.27 ⊢ ( 𝜑 → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
11 10 imdistani ⊢ ( ( 𝜑 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 ∧ 𝜓 ) )
12 11 orcd ⊢ ( ( 𝜑 ∧ ( 𝜑 → 𝜓 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
13 12 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
14 pm2.27 ⊢ ( ¬ 𝜑 → ( ( ¬ 𝜑 → 𝜒 ) → 𝜒 ) )
15 14 imdistani ⊢ ( ( ¬ 𝜑 ∧ ( ¬ 𝜑 → 𝜒 ) ) → ( ¬ 𝜑 ∧ 𝜒 ) )
16 15 olcd ⊢ ( ( ¬ 𝜑 ∧ ( ¬ 𝜑 → 𝜒 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
17 16 adantrl ⊢ ( ( ¬ 𝜑 ∧ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
18 13 17 pm2.61ian ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
19 9 18 impbii ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )