Theorem ifbieq1d 4500

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 4499	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3		ifbieq1d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq1d 4495	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
5	2, 4	eqtrd 2766	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-un 3907  df-if 4476

This theorem is referenced by:  opeq1  4825  opeq2  4826  oieq1  9398  oieq2  9399  cantnflem1d  9578  cantnflem1  9579  ttrcltr  9606  iunfictbso  10005  ttukey2g  10407  bcval  14211  swrdval  14551  summolem2a  15622  zsum  15625  fsum  15627  sumss  15631  sumss2  15633  fsumcvg2  15634  fsumser  15637  isumless  15752  cbvprod  15820  cbvprodv  15821  prodmolem2a  15841  zprod  15844  fprod  15848  fprodntriv  15849  prodss  15854  rpnnen2lem1  16123  sadadd2lem  16370  sadadd2  16371  pcmpt  16804  pcmptdvds  16806  prmreclem2  16829  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  prmrec  16834  ramub1lem2  16939  ramcl  16941  prmop1  16950  prmonn2  16951  prmdvdsprmo  16954  fvprmselelfz  16956  fvprmselgcd1  16957  prmodvdslcmf  16959  prmgapprmo  16974  smndex2dlinvh  18825  pmtrval  19364  pmtrdifellem3  19391  cyggenod2  19798  gsummpt1n0  19878  dmdprdsplitlem  19952  cycsubggenodd  20024  cyggic  21510  evlslem2  22015  coe1tmmul2fv  22193  coe1pwmulfv  22195  dmatmulcl  22416  scmatscmiddistr  22424  marrepval  22478  maducoeval  22555  maducoeval2  22556  minmar1val  22564  fclsval  23924  stdbdmetval  24430  stdbdxmet  24431  pcopt2  24951  cmetcaulem  25216  ovolicc2lem3  25448  ovolicc2lem4  25449  ovolicc2lem5  25450  mbfposb  25582  i1fres  25634  i1fposd  25636  mbfi1fseqlem2  25645  mbfi1fseq  25650  mbfi1flimlem  25651  mbfi1flim  25652  itg2splitlem  25677  itg2cnlem1  25690  itg2cn  25692  isibl  25694  isibl2  25695  iblitg  25697  dfitg  25698  cbvitg  25705  itgeq2  25707  itgvallem  25714  iblneg  25732  itgneg  25733  itgss3  25744  itgcn  25774  deg1suble  26040  elply2  26129  dgrsub  26206  aareccl  26262  vmaval  27051  prmorcht  27116  pclogsum  27154  dchrelbasd  27178  dchrptlem2  27204  bposlem5  27227  lgsfval  27241  lgsdir  27271  lgsdilem2  27272  lgsdi  27273  lgsne0  27274  rplogsumlem2  27424  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  elrspunsn  33392  gsummoncoe1fzo  33556  fldextrspunlsp  33685  extdgfialglem2  33704  ballotlemsval  34520  ballotlemieq  34528  mrsubfval  35550  cbvprodvw2  36287  cbvproddavw  36320  cbvsumdavw2  36335  cbvproddavw2  36336  poimirlem1  37667  poimirlem5  37671  poimirlem6  37672  poimirlem12  37678  poimirlem22  37688  mblfinlem2  37704  itg2addnclem  37717  ftc1anclem5  37743  ftc1anclem6  37744  cdlemk40  40962  fsuppind  42629  cantnfub  43360  dvnprodlem1  45990  fourierdlem86  46236  fourierdlem97  46247  fourierdlem103  46253  fourierdlem104  46254  fourierdlem112  46262  isomennd  46575  hsphoif  46620  hsphoival  46623  sge0hsphoire  46633  hoidmv1lelem2  46636  hoidmv1lelem3  46637  hoidmv1le  46638  hoidmvlelem1  46639  hoidmvlelem2  46640  hoidmvlelem3  46641  hoidmvlelem4  46642  hoidmvlelem5  46643  hspval  46653  hoidifhspval2  46659  hoidifhspval3  46663  hspmbllem2  46671  afveq12d  47170  discsubc  49102  oppfvalg  49164