Theorem ifbieq1d 4510

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-un 4154  df-if 4486

This theorem is used by:  opeq1  4843  opeq2  4844  oieq1  9530  oieq2  9531  cantnflem1d  9713  cantnflem1  9714  ttrcltr  9741  iunfictbso  10217  ttukey2g  10618  bcval  14472  swrdval  14816  summolem2a  15907  zsum  15910  fsum  15912  sumss  15916  sumss2  15918  fsumcvg2  15919  fsumser  15922  isumless  16040  cbvprod  16108  cbvprodv  16109  prodmolem2a  16127  zprod  16130  fprod  16134  fprodntriv  16135  prodss  16140  rpnnen2lem1  16408  sadadd2lem  16655  sadadd2  16656  pcmpt  17096  pcmptdvds  17098  prmreclem2  17121  prmreclem4  17123  prmreclem5  17124  prmreclem6  17125  prmrec  17126  ramub1lem2  17231  ramcl  17233  prmop1  17242  prmonn2  17243  prmdvdsprmo  17246  fvprmselelfz  17248  fvprmselgcd1  17249  prmodvdslcmf  17251  prmgapprmo  17266  smndex2dlinvh  19142  pmtrval  19692  pmtrdifellem3  19719  cyggenod2  20126  gsummpt1n0  20206  dmdprdsplitlem  20280  cycsubggenodd  20352  cyggic  21905  evlslem2  22415  coe1tmmul2fv  22624  coe1pwmulfv  22626  dmatmulcl  22842  scmatscmiddistr  22850  marrepval  22904  maducoeval  22981  maducoeval2  22982  minmar1val  22990  fclsval  24354  stdbdmetval  24860  stdbdxmet  24861  pcopt2  25371  cmetcaulem  25636  ovolicc2lem3  25867  ovolicc2lem4  25868  ovolicc2lem5  25869  mbfposb  26001  i1fres  26053  i1fposd  26055  mbfi1fseqlem2  26064  mbfi1fseq  26069  mbfi1flimlem  26070  mbfi1flim  26071  itg2splitlem  26096  itg2cnlem1  26109  itg2cn  26111  isibl  26113  isibl2  26114  iblitg  26116  dfitg  26117  cbvitg  26123  itgeq2  26125  itgvallem  26132  iblneg  26150  itgneg  26151  itgss3  26162  itgcn  26192  deg1suble  26452  elply2  26541  dgrsub  26618  aareccl  26680  vmaval  27467  prmorcht  27532  pclogsum  27569  dchrelbasd  27593  dchrptlem2  27619  bposlem5  27642  lgsfval  27656  lgsdir  27686  lgsdilem2  27687  lgsdi  27688  lgsne0  27689  rplogsumlem2  27839  pntrlog2bndlem4  27934  pntrlog2bndlem5  27935  elrspunsn  34046  gsummoncoe1fzo  34196  selvply1rhmlem2  34220  extvfval  34231  extvfvv  34233  fldextrspunlsp  34373  extdgfialglem2  34392  ballotlemsval  35208  ballotlemieq  35216  mrsubfval  36439  cbvprodvw2  37213  cbvproddavw  37246  cbvsumdavw2  37261  cbvproddavw2  37262  poimirlem1  38730  poimirlem5  38734  poimirlem6  38735  poimirlem12  38741  poimirlem22  38751  mblfinlem2  38767  itg2addnclem  38780  ftc1anclem5  38806  ftc1anclem6  38807  cdlemk40  42165  fsuppind  43809  cantnfub  44513  dvnprodlem1  47159  fourierdlem86  47405  fourierdlem97  47416  fourierdlem103  47422  fourierdlem104  47423  fourierdlem112  47431  isomennd  47744  hsphoif  47789  hsphoival  47792  sge0hsphoire  47802  hoidmv1lelem2  47805  hoidmv1lelem3  47806  hoidmv1le  47807  hoidmvlelem1  47808  hoidmvlelem2  47809  hoidmvlelem3  47810  hoidmvlelem4  47811  hoidmvlelem5  47812  hspval  47822  hoidifhspval2  47828  hoidifhspval3  47832  hspmbllem2  47840  afveq12d  48406  discsubc  50381  oppfvalg  50445