Theorem ifbi 4107

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

Assertion

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

Proof of Theorem ifbi

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  ifbid  4108  ifbieq2i  4110  gsummoncoe1  19674  scmatscm  20319  mulmarep1gsum1  20379  madugsum  20449  mp2pm2mplem4  20614  dchrhash  24996  lgsdi  25059  rpvmasum2  25201  bj-projval  32984  matunitlindflem2  33406  itg2gt0cn  33465  dedths  34248