Theorem elimifd

Description: Elimination of a conditional operator contained in a wff ch . (Contributed by Thierry Arnoux, 25-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		elimifd.1	|- ( ph -> ( if ( ps , A , B ) = A -> ( ch <-> th ) ) )
2		elimifd.2	|- ( ph -> ( if ( ps , A , B ) = B -> ( ch <-> ta ) ) )
3		exmid	|- ( ps \/ -. ps )
4	3	biantrur	|- ( ch <-> ( ( ps \/ -. ps ) /\ ch ) )
5	4	a1i	|- ( ph -> ( ch <-> ( ( ps \/ -. ps ) /\ ch ) ) )
6		andir	|- ( ( ( ps \/ -. ps ) /\ ch ) <-> ( ( ps /\ ch ) \/ ( -. ps /\ ch ) ) )
7	6	a1i	|- ( ph -> ( ( ( ps \/ -. ps ) /\ ch ) <-> ( ( ps /\ ch ) \/ ( -. ps /\ ch ) ) ) )
8		iftrue	|- ( ps -> if ( ps , A , B ) = A )
9	8 1	syl5	|- ( ph -> ( ps -> ( ch <-> th ) ) )
10	9	pm5.32d	|- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )
11		iffalse	|- ( -. ps -> if ( ps , A , B ) = B )
12	11 2	syl5	|- ( ph -> ( -. ps -> ( ch <-> ta ) ) )
13	12	pm5.32d	|- ( ph -> ( ( -. ps /\ ch ) <-> ( -. ps /\ ta ) ) )
14	10 13	orbi12d	|- ( ph -> ( ( ( ps /\ ch ) \/ ( -. ps /\ ch ) ) <-> ( ( ps /\ th ) \/ ( -. ps /\ ta ) ) ) )
15	5 7 14	3bitrd	|- ( ph -> ( ch <-> ( ( ps /\ th ) \/ ( -. ps /\ ta ) ) ) )