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	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		pm3.4	|- ( ( ph /\ ps ) -> ( ph -> ps ) )
2		pm2.24	|- ( ph -> ( -. ph -> ch ) )
3	2	adantr	|- ( ( ph /\ ps ) -> ( -. ph -> ch ) )
4	1 3	jca	|- ( ( ph /\ ps ) -> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
5		pm2.21	|- ( -. ph -> ( ph -> ps ) )
6	5	adantr	|- ( ( -. ph /\ ch ) -> ( ph -> ps ) )
7		pm3.4	|- ( ( -. ph /\ ch ) -> ( -. ph -> ch ) )
8	6 7	jca	|- ( ( -. ph /\ ch ) -> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
9	4 8	jaoi	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
10		pm2.27	|- ( ph -> ( ( ph -> ps ) -> ps ) )
11	10	imdistani	|- ( ( ph /\ ( ph -> ps ) ) -> ( ph /\ ps ) )
12	11	orcd	|- ( ( ph /\ ( ph -> ps ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
13	12	adantrr	|- ( ( ph /\ ( ( ph -> ps ) /\ ( -. ph -> ch ) ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
14		pm2.27	|- ( -. ph -> ( ( -. ph -> ch ) -> ch ) )
15	14	imdistani	|- ( ( -. ph /\ ( -. ph -> ch ) ) -> ( -. ph /\ ch ) )
16	15	olcd	|- ( ( -. ph /\ ( -. ph -> ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
17	16	adantrl	|- ( ( -. ph /\ ( ( ph -> ps ) /\ ( -. ph -> ch ) ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
18	13 17	pm2.61ian	|- ( ( ( ph -> ps ) /\ ( -. ph -> ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
19	9 18	impbii	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )