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 2791	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1554  ifcif 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-un 3904  df-if 4475

This theorem is referenced by:  opeq1  4825  opeq2  4826  oieq1  9450  oieq2  9451  cantnflem1d  9633  cantnflem1  9634  ttrcltr  9661  iunfictbso  10060  ttukey2g  10463  bcval  14307  swrdval  14647  summolem2a  15718  zsum  15721  fsum  15723  sumss  15727  sumss2  15729  fsumcvg2  15730  fsumser  15733  isumless  15851  cbvprod  15919  cbvprodv  15920  prodmolem2a  15940  zprod  15943  fprod  15947  fprodntriv  15948  prodss  15953  rpnnen2lem1  16222  sadadd2lem  16469  sadadd2  16470  pcmpt  16904  pcmptdvds  16906  prmreclem2  16929  prmreclem4  16931  prmreclem5  16932  prmreclem6  16933  prmrec  16934  ramub1lem2  17039  ramcl  17041  prmop1  17050  prmonn2  17051  prmdvdsprmo  17054  fvprmselelfz  17056  fvprmselgcd1  17057  prmodvdslcmf  17059  prmgapprmo  17074  smndex2dlinvh  18930  pmtrval  19467  pmtrdifellem3  19494  cyggenod2  19901  gsummpt1n0  19981  dmdprdsplitlem  20055  cycsubggenodd  20127  cyggic  21597  evlslem2  22105  coe1tmmul2fv  22314  coe1pwmulfv  22316  dmatmulcl  22533  scmatscmiddistr  22541  marrepval  22595  maducoeval  22672  maducoeval2  22673  minmar1val  22681  fclsval  24041  stdbdmetval  24547  stdbdxmet  24548  pcopt2  25058  cmetcaulem  25323  ovolicc2lem3  25554  ovolicc2lem4  25555  ovolicc2lem5  25556  mbfposb  25688  i1fres  25740  i1fposd  25742  mbfi1fseqlem2  25751  mbfi1fseq  25756  mbfi1flimlem  25757  mbfi1flim  25758  itg2splitlem  25783  itg2cnlem1  25796  itg2cn  25798  isibl  25800  isibl2  25801  iblitg  25803  dfitg  25804  cbvitg  25811  itgeq2  25813  itgvallem  25820  iblneg  25838  itgneg  25839  itgss3  25850  itgcn  25880  deg1suble  26140  elply2  26229  dgrsub  26305  aareccl  26360  vmaval  27147  prmorcht  27212  pclogsum  27249  dchrelbasd  27273  dchrptlem2  27299  bposlem5  27322  lgsfval  27336  lgsdir  27366  lgsdilem2  27367  lgsdi  27368  lgsne0  27369  rplogsumlem2  27519  pntrlog2bndlem4  27614  pntrlog2bndlem5  27615  elrspunsn  33569  gsummoncoe1fzo  33747  selvply1rhmlem2  33772  extvfval  33783  extvfvv  33785  fldextrspunlsp  33925  extdgfialglem2  33944  ballotlemsval  34760  ballotlemieq  34768  mrsubfval  35806  cbvprodvw2  36555  cbvproddavw  36588  cbvsumdavw2  36603  cbvproddavw2  36604  poimirlem1  38068  poimirlem5  38072  poimirlem6  38073  poimirlem12  38079  poimirlem22  38089  mblfinlem2  38105  itg2addnclem  38118  ftc1anclem5  38144  ftc1anclem6  38145  cdlemk40  41489  fsuppind  43120  cantnfub  43846  dvnprodlem1  46468  fourierdlem86  46714  fourierdlem97  46725  fourierdlem103  46731  fourierdlem104  46732  fourierdlem112  46740  isomennd  47053  hsphoif  47098  hsphoival  47101  sge0hsphoire  47111  hoidmv1lelem2  47114  hoidmv1lelem3  47115  hoidmv1le  47116  hoidmvlelem1  47117  hoidmvlelem2  47118  hoidmvlelem3  47119  hoidmvlelem4  47120  hoidmvlelem5  47121  hspval  47131  hoidifhspval2  47137  hoidifhspval3  47141  hspmbllem2  47149  afveq12d  47675  discsubc  49633  oppfvalg  49695