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

Metamath Proof Explorer

Theorem cases

Description: Case disjunction according to the value of ph . (Contributed by NM, 25-Apr-2019)

Ref Expression
Hypotheses cases.1 
|- ( ph -> ( ps <-> ch ) )
cases.2 
|- ( -. ph -> ( ps <-> th ) )
Assertion cases 
|- ( ps <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )

Proof

Step Hyp Ref Expression
1 cases.1 
 |-  ( ph -> ( ps <-> ch ) )
2 cases.2 
 |-  ( -. ph -> ( ps <-> th ) )
3 exmid 
 |-  ( ph \/ -. ph )
4 3 biantrur 
 |-  ( ps <-> ( ( ph \/ -. ph ) /\ ps ) )
5 andir 
 |-  ( ( ( ph \/ -. ph ) /\ ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ps ) ) )
6 1 pm5.32i 
 |-  ( ( ph /\ ps ) <-> ( ph /\ ch ) )
7 2 pm5.32i 
 |-  ( ( -. ph /\ ps ) <-> ( -. ph /\ th ) )
8 6 7 orbi12i 
 |-  ( ( ( ph /\ ps ) \/ ( -. ph /\ ps ) ) <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )
9 4 5 8 3bitri 
 |-  ( ps <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )