Theorem ifbieq1d 4503

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-un 3910  df-if 4479

This theorem is referenced by:  opeq1  4827  opeq2  4828  oieq1  9423  oieq2  9424  cantnflem1d  9603  cantnflem1  9604  ttrcltr  9631  iunfictbso  10027  ttukey2g  10429  bcval  14229  swrdval  14568  summolem2a  15640  zsum  15643  fsum  15645  sumss  15649  sumss2  15651  fsumcvg2  15652  fsumser  15655  isumless  15770  cbvprod  15838  cbvprodv  15839  prodmolem2a  15859  zprod  15862  fprod  15866  fprodntriv  15867  prodss  15872  rpnnen2lem1  16141  sadadd2lem  16388  sadadd2  16389  pcmpt  16822  pcmptdvds  16824  prmreclem2  16847  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  prmrec  16852  ramub1lem2  16957  ramcl  16959  prmop1  16968  prmonn2  16969  prmdvdsprmo  16972  fvprmselelfz  16974  fvprmselgcd1  16975  prmodvdslcmf  16977  prmgapprmo  16992  smndex2dlinvh  18809  pmtrval  19348  pmtrdifellem3  19375  cyggenod2  19782  gsummpt1n0  19862  dmdprdsplitlem  19936  cycsubggenodd  20008  cyggic  21497  evlslem2  22002  coe1tmmul2fv  22180  coe1pwmulfv  22182  dmatmulcl  22403  scmatscmiddistr  22411  marrepval  22465  maducoeval  22542  maducoeval2  22543  minmar1val  22551  fclsval  23911  stdbdmetval  24418  stdbdxmet  24419  pcopt2  24939  cmetcaulem  25204  ovolicc2lem3  25436  ovolicc2lem4  25437  ovolicc2lem5  25438  mbfposb  25570  i1fres  25622  i1fposd  25624  mbfi1fseqlem2  25633  mbfi1fseq  25638  mbfi1flimlem  25639  mbfi1flim  25640  itg2splitlem  25665  itg2cnlem1  25678  itg2cn  25680  isibl  25682  isibl2  25683  iblitg  25685  dfitg  25686  cbvitg  25693  itgeq2  25695  itgvallem  25702  iblneg  25720  itgneg  25721  itgss3  25732  itgcn  25762  deg1suble  26028  elply2  26117  dgrsub  26194  aareccl  26250  vmaval  27039  prmorcht  27104  pclogsum  27142  dchrelbasd  27166  dchrptlem2  27192  bposlem5  27215  lgsfval  27229  lgsdir  27259  lgsdilem2  27260  lgsdi  27261  lgsne0  27262  rplogsumlem2  27412  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  elrspunsn  33379  gsummoncoe1fzo  33542  fldextrspunlsp  33648  ballotlemsval  34479  ballotlemieq  34487  mrsubfval  35483  cbvprodvw2  36223  cbvproddavw  36256  cbvsumdavw2  36271  cbvproddavw2  36272  poimirlem1  37603  poimirlem5  37607  poimirlem6  37608  poimirlem12  37614  poimirlem22  37624  mblfinlem2  37640  itg2addnclem  37653  ftc1anclem5  37679  ftc1anclem6  37680  cdlemk40  40899  fsuppind  42566  cantnfub  43297  dvnprodlem1  45931  fourierdlem86  46177  fourierdlem97  46188  fourierdlem103  46194  fourierdlem104  46195  fourierdlem112  46203  isomennd  46516  hsphoif  46561  hsphoival  46564  sge0hsphoire  46574  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmv1le  46579  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem3  46582  hoidmvlelem4  46583  hoidmvlelem5  46584  hspval  46594  hoidifhspval2  46600  hoidifhspval3  46604  hspmbllem2  46612  afveq12d  47121  discsubc  49053  oppfvalg  49115