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

Proof

Step Hyp Ref Expression
1 pm4.83 
 |-  ( ( ( ph -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) /\ ( -. ph -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) ) <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) )
2 dedlema 
 |-  ( ph -> ( ps <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
3 2 pm5.74i 
 |-  ( ( ph -> ps ) <-> ( ph -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
4 dedlemb 
 |-  ( -. ph -> ( ch <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
5 4 pm5.74i 
 |-  ( ( -. ph -> ch ) <-> ( -. ph -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
6 3 5 anbi12i 
 |-  ( ( ( ph -> ps ) /\ ( -. ph -> ch ) ) <-> ( ( ph -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) /\ ( -. ph -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) ) )
7 ancom 
 |-  ( ( ph /\ ps ) <-> ( ps /\ ph ) )
8 ancom 
 |-  ( ( -. ph /\ ch ) <-> ( ch /\ -. ph ) )
9 7 8 orbi12i 
 |-  ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) )
10 1 6 9 3bitr4ri 
 |-  ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )