Theorem elim2ifim 28165

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

Hypotheses

Ref	Expression
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

Ref	Expression
elim2ifim	|- ch

Proof of Theorem elim2ifim

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   = wceq 1437   ifcif 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-if 3912

This theorem is referenced by: (None)