Metamath Proof Explorer

Theorem elim2ifim

Description: Elimination of two conditional operators for an implication. (Contributed by Thierry Arnoux, 25-Jan-2017)

Ref Expression
Hypotheses elim2if.1 
|- ( if ( ph , A , if ( ps , B , C ) ) = A -> ( ch <-> th ) )
elim2if.2 
|- ( if ( ph , A , if ( ps , B , C ) ) = B -> ( ch <-> ta ) )
elim2if.3 
|- ( if ( ph , A , if ( ps , B , C ) ) = C -> ( ch <-> et ) )
elim2ifim.1 
|- ( ph -> th )
elim2ifim.2 
|- ( ( -. ph /\ ps ) -> ta )
elim2ifim.3 
|- ( ( -. ph /\ -. ps ) -> et )
Assertion elim2ifim 
|- ch

Proof

Step Hyp Ref Expression
1 elim2if.1 
 |-  ( if ( ph , A , if ( ps , B , C ) ) = A -> ( ch <-> th ) )
2 elim2if.2 
 |-  ( if ( ph , A , if ( ps , B , C ) ) = B -> ( ch <-> ta ) )
3 elim2if.3 
 |-  ( if ( ph , A , if ( ps , B , C ) ) = C -> ( ch <-> et ) )
4 elim2ifim.1 
 |-  ( ph -> th )
5 elim2ifim.2 
 |-  ( ( -. ph /\ ps ) -> ta )
6 elim2ifim.3 
 |-  ( ( -. ph /\ -. ps ) -> et )
7 exmid 
 |-  ( ph \/ -. ph )
8 4 ancli 
 |-  ( ph -> ( ph /\ th ) )
9 pm4.42 
 |-  ( -. ph <-> ( ( -. ph /\ ps ) \/ ( -. ph /\ -. ps ) ) )
10 5 ex 
 |-  ( -. ph -> ( ps -> ta ) )
11 10 ancld 
 |-  ( -. ph -> ( ps -> ( ps /\ ta ) ) )
12 11 imp 
 |-  ( ( -. ph /\ ps ) -> ( ps /\ ta ) )
13 6 ex 
 |-  ( -. ph -> ( -. ps -> et ) )
14 13 ancld 
 |-  ( -. ph -> ( -. ps -> ( -. ps /\ et ) ) )
15 14 imp 
 |-  ( ( -. ph /\ -. ps ) -> ( -. ps /\ et ) )
16 12 15 orim12i 
 |-  ( ( ( -. ph /\ ps ) \/ ( -. ph /\ -. ps ) ) -> ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) )
17 9 16 sylbi 
 |-  ( -. ph -> ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) )
18 17 ancli 
 |-  ( -. ph -> ( -. ph /\ ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) )
19 8 18 orim12i 
 |-  ( ( ph \/ -. ph ) -> ( ( ph /\ th ) \/ ( -. ph /\ ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) ) )
20 7 19 ax-mp 
 |-  ( ( ph /\ th ) \/ ( -. ph /\ ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) )
21 1 2 3 elim2if 
 |-  ( ch <-> ( ( ph /\ th ) \/ ( -. ph /\ ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) ) )
22 20 21 mpbir 
 |-  ch