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 ( ( ( 𝜑𝜓 ) ∨ ( ¬ 𝜑𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ∧ ( ¬ 𝜑𝜒 ) ) )