Theorem ifbieq1d 4483

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

Hypotheses

Ref	Expression
ifbieq1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq1d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifbieq1d	⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Proof of Theorem ifbieq1d

Step	Hyp	Ref	Expression
1		ifbieq1d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 4482	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3		ifbieq1d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq1d 4478	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
5	2, 4	eqtrd 2778	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-un 3892  df-if 4460

This theorem is referenced by:  opeq1  4804  opeq2  4805  oieq1  9271  oieq2  9272  cantnflem1d  9446  cantnflem1  9447  ttrcltr  9474  iunfictbso  9870  ttukey2g  10272  bcval  14018  swrdval  14356  summolem2a  15427  zsum  15430  fsum  15432  sumss  15436  sumss2  15438  fsumcvg2  15439  fsumser  15442  isumless  15557  cbvprod  15625  prodmolem2a  15644  zprod  15647  fprod  15651  fprodntriv  15652  prodss  15657  rpnnen2lem1  15923  sadadd2lem  16166  sadadd2  16167  pcmpt  16593  pcmptdvds  16595  prmreclem2  16618  prmreclem4  16620  prmreclem5  16621  prmreclem6  16622  prmrec  16623  ramub1lem2  16728  ramcl  16730  prmop1  16739  prmonn2  16740  prmdvdsprmo  16743  fvprmselelfz  16745  fvprmselgcd1  16746  prmodvdslcmf  16748  prmgapprmo  16763  smndex2dlinvh  18556  pmtrval  19059  pmtrdifellem3  19086  cyggenod2  19485  gsummpt1n0  19566  dmdprdsplitlem  19640  cycsubggenodd  19712  cyggic  20780  evlslem2  21289  coe1tmmul2fv  21449  coe1pwmulfv  21451  dmatmulcl  21649  scmatscmiddistr  21657  marrepval  21711  maducoeval  21788  maducoeval2  21789  minmar1val  21797  fclsval  23159  stdbdmetval  23670  stdbdxmet  23671  pcopt2  24186  cmetcaulem  24452  ovolicc2lem3  24683  ovolicc2lem4  24684  ovolicc2lem5  24685  mbfposb  24817  i1fres  24870  i1fposd  24872  mbfi1fseqlem2  24881  mbfi1fseq  24886  mbfi1flimlem  24887  mbfi1flim  24888  itg2splitlem  24913  itg2cnlem1  24926  itg2cn  24928  isibl  24930  isibl2  24931  iblitg  24933  dfitg  24934  cbvitg  24940  itgeq2  24942  itgvallem  24949  iblneg  24967  itgneg  24968  itgss3  24979  itgcn  25009  deg1suble  25272  elply2  25357  dgrsub  25433  aareccl  25486  vmaval  26262  prmorcht  26327  pclogsum  26363  dchrelbasd  26387  dchrptlem2  26413  bposlem5  26436  lgsfval  26450  lgsdir  26480  lgsdilem2  26481  lgsdi  26482  lgsne0  26483  rplogsumlem2  26633  pntrlog2bndlem4  26728  pntrlog2bndlem5  26729  ballotlemsval  32475  ballotlemieq  32483  mrsubfval  33470  poimirlem1  35778  poimirlem5  35782  poimirlem6  35783  poimirlem12  35789  poimirlem22  35799  mblfinlem2  35815  itg2addnclem  35828  ftc1anclem5  35854  ftc1anclem6  35855  cdlemk40  38931  fsuppind  40279  dvnprodlem1  43487  fourierdlem86  43733  fourierdlem97  43744  fourierdlem103  43750  fourierdlem104  43751  fourierdlem112  43759  isomennd  44069  hsphoif  44114  hsphoival  44117  sge0hsphoire  44127  hoidmv1lelem2  44130  hoidmv1lelem3  44131  hoidmv1le  44132  hoidmvlelem1  44133  hoidmvlelem2  44134  hoidmvlelem3  44135  hoidmvlelem4  44136  hoidmvlelem5  44137  hspval  44147  hoidifhspval2  44153  hoidifhspval3  44157  hspmbllem2  44165  afveq12d  44625