This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ifbi

Description: Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004)

Ref Expression
Assertion ifbi 
|- ( ( ph <-> ps ) -> if ( ph , A , B ) = if ( ps , A , B ) )

Proof

Step Hyp Ref Expression
1 dfbi3 
 |-  ( ( ph <-> ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) )
2 iftrue 
 |-  ( ph -> if ( ph , A , B ) = A )
3 iftrue 
 |-  ( ps -> if ( ps , A , B ) = A )
4 3 eqcomd 
 |-  ( ps -> A = if ( ps , A , B ) )
5 2 4 sylan9eq 
 |-  ( ( ph /\ ps ) -> if ( ph , A , B ) = if ( ps , A , B ) )
6 iffalse 
 |-  ( -. ph -> if ( ph , A , B ) = B )
7 iffalse 
 |-  ( -. ps -> if ( ps , A , B ) = B )
8 7 eqcomd 
 |-  ( -. ps -> B = if ( ps , A , B ) )
9 6 8 sylan9eq 
 |-  ( ( -. ph /\ -. ps ) -> if ( ph , A , B ) = if ( ps , A , B ) )
10 5 9 jaoi 
 |-  ( ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) -> if ( ph , A , B ) = if ( ps , A , B ) )
11 1 10 sylbi 
 |-  ( ( ph <-> ps ) -> if ( ph , A , B ) = if ( ps , A , B ) )