Theorem elim2if

Description: Elimination of two conditional operators contained in a wff ch . (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 ) )
Assertion	elim2if	|- ( ch <-> ( ( ph /\ th ) \/ ( -. ph /\ ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) ) )

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		iftrue	|- ( ph -> if ( ph , A , if ( ps , B , C ) ) = A )
5	4 1	syl	|- ( ph -> ( ch <-> th ) )
6		iffalse	|- ( -. ph -> if ( ph , A , if ( ps , B , C ) ) = if ( ps , B , C ) )
7	6	eqeq1d	|- ( -. ph -> ( if ( ph , A , if ( ps , B , C ) ) = B <-> if ( ps , B , C ) = B ) )
8	7 2	biimtrrdi	|- ( -. ph -> ( if ( ps , B , C ) = B -> ( ch <-> ta ) ) )
9	6	eqeq1d	|- ( -. ph -> ( if ( ph , A , if ( ps , B , C ) ) = C <-> if ( ps , B , C ) = C ) )
10	9 3	biimtrrdi	|- ( -. ph -> ( if ( ps , B , C ) = C -> ( ch <-> et ) ) )
11	8 10	elimifd	|- ( -. ph -> ( ch <-> ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) )
12	5 11	cases	|- ( ch <-> ( ( ph /\ th ) \/ ( -. ph /\ ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) ) )