Theorem ifbieq1d 4481

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-un 3889  df-if 4457

This theorem is referenced by:  opeq1  4806  opeq2  4807  oieq1  9421  oieq2  9422  cantnflem1d  9604  cantnflem1  9605  ttrcltr  9632  iunfictbso  10031  ttukey2g  10434  bcval  14261  swrdval  14601  summolem2a  15672  zsum  15675  fsum  15677  sumss  15681  sumss2  15683  fsumcvg2  15684  fsumser  15687  isumless  15805  cbvprod  15873  cbvprodv  15874  prodmolem2a  15894  zprod  15897  fprod  15901  fprodntriv  15902  prodss  15907  rpnnen2lem1  16176  sadadd2lem  16423  sadadd2  16424  pcmpt  16858  pcmptdvds  16860  prmreclem2  16883  prmreclem4  16885  prmreclem5  16886  prmreclem6  16887  prmrec  16888  ramub1lem2  16993  ramcl  16995  prmop1  17004  prmonn2  17005  prmdvdsprmo  17008  fvprmselelfz  17010  fvprmselgcd1  17011  prmodvdslcmf  17013  prmgapprmo  17028  smndex2dlinvh  18883  pmtrval  19420  pmtrdifellem3  19447  cyggenod2  19854  gsummpt1n0  19934  dmdprdsplitlem  20008  cycsubggenodd  20080  cyggic  21550  evlslem2  22058  coe1tmmul2fv  22267  coe1pwmulfv  22269  dmatmulcl  22486  scmatscmiddistr  22494  marrepval  22548  maducoeval  22625  maducoeval2  22626  minmar1val  22634  fclsval  23994  stdbdmetval  24500  stdbdxmet  24501  pcopt2  25011  cmetcaulem  25276  ovolicc2lem3  25507  ovolicc2lem4  25508  ovolicc2lem5  25509  mbfposb  25641  i1fres  25693  i1fposd  25695  mbfi1fseqlem2  25704  mbfi1fseq  25709  mbfi1flimlem  25710  mbfi1flim  25711  itg2splitlem  25736  itg2cnlem1  25749  itg2cn  25751  isibl  25753  isibl2  25754  iblitg  25756  dfitg  25757  cbvitg  25764  itgeq2  25766  itgvallem  25773  iblneg  25791  itgneg  25792  itgss3  25803  itgcn  25833  deg1suble  26093  elply2  26182  dgrsub  26258  aareccl  26313  vmaval  27097  prmorcht  27162  pclogsum  27199  dchrelbasd  27223  dchrptlem2  27249  bposlem5  27272  lgsfval  27286  lgsdir  27316  lgsdilem2  27317  lgsdi  27318  lgsne0  27319  rplogsumlem2  27469  pntrlog2bndlem4  27564  pntrlog2bndlem5  27565  elrspunsn  33514  gsummoncoe1fzo  33690  selvply1rhmlem2  33715  extvfval  33726  extvfvv  33728  fldextrspunlsp  33868  extdgfialglem2  33887  ballotlemsval  34703  ballotlemieq  34711  mrsubfval  35749  cbvprodvw2  36488  cbvproddavw  36521  cbvsumdavw2  36536  cbvproddavw2  36537  poimirlem1  38001  poimirlem5  38005  poimirlem6  38006  poimirlem12  38012  poimirlem22  38022  mblfinlem2  38038  itg2addnclem  38051  ftc1anclem5  38077  ftc1anclem6  38078  cdlemk40  41422  fsuppind  43053  cantnfub  43779  dvnprodlem1  46401  fourierdlem86  46647  fourierdlem97  46658  fourierdlem103  46664  fourierdlem104  46665  fourierdlem112  46673  isomennd  46986  hsphoif  47031  hsphoival  47034  sge0hsphoire  47044  hoidmv1lelem2  47047  hoidmv1lelem3  47048  hoidmv1le  47049  hoidmvlelem1  47050  hoidmvlelem2  47051  hoidmvlelem3  47052  hoidmvlelem4  47053  hoidmvlelem5  47054  hspval  47064  hoidifhspval2  47070  hoidifhspval3  47074  hspmbllem2  47082  afveq12d  47608  discsubc  49566  oppfvalg  49628