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  7309  ctssdc  7312  enumctlemm  7313  iseqf1olemfvp  10773  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  bcval  11012  swrdval  11233  sumrbdclem  11956  summodclem3  11959  summodclem2a  11960  summodc  11962  zsumdc  11963  fsum3  11966  isumss  11970  isumss2  11972  fsum3cvg2  11973  fsum3ser  11976  fsumcl2lem  11977  fsumadd  11985  sumsnf  11988  fsummulc2  12027  isumlessdc  12075  cbvprod  12137  prodrbdclem  12150  prodmodclem3  12154  prodmodclem2a  12155  prodmodc  12157  zproddc  12158  fprodseq  12162  fprodntrivap  12163  prodssdc  12168  fprodmul  12170  prodsnf  12171  pcmpt  12934  pcmptdvds  12936  elply2  15478  lgsval  15752  lgsfvalg  15753  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786