Theorem ifbieq1d 4499

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

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

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-un 3903  df-if 4475

This theorem is referenced by:  opeq1  4824  opeq2  4825  oieq1  9405  oieq2  9406  cantnflem1d  9585  cantnflem1  9586  ttrcltr  9613  iunfictbso  10012  ttukey2g  10414  bcval  14213  swrdval  14553  summolem2a  15624  zsum  15627  fsum  15629  sumss  15633  sumss2  15635  fsumcvg2  15636  fsumser  15639  isumless  15754  cbvprod  15822  cbvprodv  15823  prodmolem2a  15843  zprod  15846  fprod  15850  fprodntriv  15851  prodss  15856  rpnnen2lem1  16125  sadadd2lem  16372  sadadd2  16373  pcmpt  16806  pcmptdvds  16808  prmreclem2  16831  prmreclem4  16833  prmreclem5  16834  prmreclem6  16835  prmrec  16836  ramub1lem2  16941  ramcl  16943  prmop1  16952  prmonn2  16953  prmdvdsprmo  16956  fvprmselelfz  16958  fvprmselgcd1  16959  prmodvdslcmf  16961  prmgapprmo  16976  smndex2dlinvh  18827  pmtrval  19365  pmtrdifellem3  19392  cyggenod2  19799  gsummpt1n0  19879  dmdprdsplitlem  19953  cycsubggenodd  20025  cyggic  21511  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  33401  gsummoncoe1fzo  33565  extvfval  33583  extvfvv  33585  fldextrspunlsp  33708  extdgfialglem2  33727  ballotlemsval  34543  ballotlemieq  34551  mrsubfval  35573  cbvprodvw2  36312  cbvproddavw  36345  cbvsumdavw2  36360  cbvproddavw2  36361  poimirlem1  37682  poimirlem5  37686  poimirlem6  37687  poimirlem12  37693  poimirlem22  37703  mblfinlem2  37719  itg2addnclem  37732  ftc1anclem5  37758  ftc1anclem6  37759  cdlemk40  41037  fsuppind  42709  cantnfub  43439  dvnprodlem1  46069  fourierdlem86  46315  fourierdlem97  46326  fourierdlem103  46332  fourierdlem104  46333  fourierdlem112  46341  isomennd  46654  hsphoif  46699  hsphoival  46702  sge0hsphoire  46712  hoidmv1lelem2  46715  hoidmv1lelem3  46716  hoidmv1le  46717  hoidmvlelem1  46718  hoidmvlelem2  46719  hoidmvlelem3  46720  hoidmvlelem4  46721  hoidmvlelem5  46722  hspval  46732  hoidifhspval2  46738  hoidifhspval3  46742  hspmbllem2  46750  afveq12d  47258  discsubc  49190  oppfvalg  49252