Theorem ifbieq1d 3625

Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.)

Hypotheses

Ref	Expression
ifbieq1d.1	|- ( ph -> ( ps <-> ch ) )
ifbieq1d.2	|- ( ph -> A = B )

Assertion

Ref	Expression
ifbieq1d	|- ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )

Proof of Theorem ifbieq1d

Step	Hyp	Ref	Expression
1		ifbieq1d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	ifbid 3624	. 2 |- ( ph -> if ( ps , A , C ) = if ( ch , A , C ) )
3		ifbieq1d.2	. . 3 |- ( ph -> A = B )
4	3	ifeq1d 3620	. 2 |- ( ph -> if ( ch , A , C ) = if ( ch , B , C ) )
5	2, 4	eqtrd 2262	1 |- ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   ifcif 3602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801  df-un 3201  df-if 3603

This theorem is referenced by:  ctssdclemn0  7288  ctssdc  7291  enumctlemm  7292  iseqf1olemfvp  10744  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  bcval  10983  swrdval  11195  sumrbdclem  11903  summodclem3  11906  summodclem2a  11907  summodc  11909  zsumdc  11910  fsum3  11913  isumss  11917  isumss2  11919  fsum3cvg2  11920  fsum3ser  11923  fsumcl2lem  11924  fsumadd  11932  sumsnf  11935  fsummulc2  11974  isumlessdc  12022  cbvprod  12084  prodrbdclem  12097  prodmodclem3  12101  prodmodclem2a  12102  prodmodc  12104  zproddc  12105  fprodseq  12109  fprodntrivap  12110  prodssdc  12115  fprodmul  12117  prodsnf  12118  pcmpt  12881  pcmptdvds  12883  elply2  15424  lgsval  15698  lgsfvalg  15699  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732