Theorem ifbieq1d 3628

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 3627	. 2 |- ( ph -> if ( ps , A , C ) = if ( ch , A , C ) )
3		ifbieq1d.2	. . 3 |- ( ph -> A = B )
4	3	ifeq1d 3623	. 2 |- ( ph -> if ( ch , A , C ) = if ( ch , B , C ) )
5	2, 4	eqtrd 2264	1 |- ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   ifcif 3605

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-v 2804  df-un 3204  df-if 3606

This theorem is referenced by:  ctssdclemn0  7308  ctssdc  7311  enumctlemm  7312  iseqf1olemfvp  10771  seq3f1olemqsum  10774  seq3f1oleml  10777  seq3f1o  10778  bcval  11010  swrdval  11228  sumrbdclem  11937  summodclem3  11940  summodclem2a  11941  summodc  11943  zsumdc  11944  fsum3  11947  isumss  11951  isumss2  11953  fsum3cvg2  11954  fsum3ser  11957  fsumcl2lem  11958  fsumadd  11966  sumsnf  11969  fsummulc2  12008  isumlessdc  12056  cbvprod  12118  prodrbdclem  12131  prodmodclem3  12135  prodmodclem2a  12136  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodntrivap  12144  prodssdc  12149  fprodmul  12151  prodsnf  12152  pcmpt  12915  pcmptdvds  12917  elply2  15458  lgsval  15732  lgsfvalg  15733  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766