Theorem elim2ifim 27125

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 415	. . 3 |- ( ph \/ -. ph )
2		elim2ifim.1	. . . . 5 |- ( ph -> th )
3	2	ancli 551	. . . 4 |- ( ph -> ( ph /\ th ) )
4		pm4.42 958	. . . . . 6 |- ( -. ph <-> ( ( -. ph /\ ps ) \/ ( -. ph /\ -. ps ) ) )
5		elim2ifim.2	. . . . . . . . . 10 |- ( ( -. ph /\ ps ) -> ta )
6	5	ex 434	. . . . . . . . 9 |- ( -. ph -> ( ps -> ta ) )
7	6	ancld 553	. . . . . . . 8 |- ( -. ph -> ( ps -> ( ps /\ ta ) ) )
8	7	imp 429	. . . . . . 7 |- ( ( -. ph /\ ps ) -> ( ps /\ ta ) )
9		elim2ifim.3	. . . . . . . . . 10 |- ( ( -. ph /\ -. ps ) -> et )
10	9	ex 434	. . . . . . . . 9 |- ( -. ph -> ( -. ps -> et ) )
11	10	ancld 553	. . . . . . . 8 |- ( -. ph -> ( -. ps -> ( -. ps /\ et ) ) )
12	11	imp 429	. . . . . . 7 |- ( ( -. ph /\ -. ps ) -> ( -. ps /\ et ) )
13	8, 12	orim12i 516	. . . . . 6 |- ( ( ( -. ph /\ ps ) \/ ( -. ph /\ -. ps ) ) -> ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) )
14	4, 13	sylbi 195	. . . . 5 |- ( -. ph -> ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) )
15	14	ancli 551	. . . 4 |- ( -. ph -> ( -. ph /\ ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) )
16	3, 15	orim12i 516	. . 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 27124	. 2 |- ( ch <-> ( ( ph /\ th ) \/ ( -. ph /\ ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) ) )
22	17, 21	mpbir 209	1 |- ch

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1379   ifcif 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940

This theorem is referenced by: (None)