Theorem elim2ifim 27401

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 960	. . . . . 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 27400	. 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 1383   ifcif 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-if 3927

This theorem is referenced by: (None)