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