Metamath Proof Explorer


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 ) ) ) )