Theorem ifbieq1d 4329

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601  ifcif 4306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-rab 3098  df-v 3399  df-un 3796  df-if 4307

This theorem is referenced by:  opeq1  4636  opeq2  4637  oieq1  8706  oieq2  8707  cantnflem1d  8882  cantnflem1  8883  iunfictbso  9270  ttukey2g  9673  bcval  13409  swrdval  13733  summolem2a  14853  zsum  14856  fsum  14858  sumss  14862  sumss2  14864  fsumcvg2  14865  fsumser  14868  isumless  14981  cbvprod  15048  prodmolem2a  15067  zprod  15070  fprod  15074  fprodntriv  15075  prodss  15080  rpnnen2lem1  15347  sadadd2lem  15587  sadadd2  15588  pcmpt  16000  pcmptdvds  16002  prmreclem2  16025  prmreclem4  16027  prmreclem5  16028  prmreclem6  16029  prmrec  16030  ramub1lem2  16135  ramcl  16137  prmop1  16146  prmonn2  16147  prmdvdsprmo  16150  fvprmselelfz  16152  fvprmselgcd1  16153  prmodvdslcmf  16155  prmgapprmo  16170  pmtrval  18254  pmtrdifellem3  18281  cyggenod2  18673  gsummpt1n0  18750  dmdprdsplitlem  18823  evlslem2  19908  coe1tmmul2fv  20044  coe1pwmulfv  20046  cyggic  20316  dmatmulcl  20711  scmatscmiddistr  20719  marrepval  20773  maducoeval  20850  maducoeval2  20851  minmar1val  20859  fclsval  22220  stdbdmetval  22727  stdbdxmet  22728  pcopt2  23230  cmetcaulem  23494  ovolicc2lem3  23723  ovolicc2lem4  23724  ovolicc2lem5  23725  mbfposb  23857  i1fres  23909  i1fposd  23911  mbfi1fseqlem2  23920  mbfi1fseq  23925  mbfi1flimlem  23926  mbfi1flim  23927  itg2splitlem  23952  itg2cnlem1  23965  itg2cn  23967  isibl  23969  isibl2  23970  iblitg  23972  dfitg  23973  cbvitg  23979  itgeq2  23981  itgvallem  23988  iblneg  24006  itgneg  24007  itgss3  24018  itgcn  24046  deg1suble  24304  elply2  24389  dgrsub  24465  aareccl  24518  vmaval  25291  prmorcht  25356  pclogsum  25392  dchrelbasd  25416  dchrptlem2  25442  bposlem5  25465  lgsfval  25479  lgsdir  25509  lgsdilem2  25510  lgsdi  25511  lgsne0  25512  rplogsumlem2  25626  pntrlog2bndlem4  25721  pntrlog2bndlem5  25722  ballotlemsval  31169  ballotlemieq  31177  mrsubfval  32004  poimirlem1  34020  poimirlem5  34024  poimirlem6  34025  poimirlem12  34031  poimirlem22  34041  mblfinlem2  34057  itg2addnclem  34070  ftc1anclem5  34098  ftc1anclem6  34099  cdlemk40  37055  dvnprodlem1  41071  fourierdlem86  41318  fourierdlem97  41329  fourierdlem103  41335  fourierdlem104  41336  fourierdlem112  41344  isomennd  41654  hsphoif  41699  hsphoival  41702  sge0hsphoire  41712  hoidmv1lelem2  41715  hoidmv1lelem3  41716  hoidmv1le  41717  hoidmvlelem1  41718  hoidmvlelem2  41719  hoidmvlelem3  41720  hoidmvlelem4  41721  hoidmvlelem5  41722  hspval  41732  hoidifhspval2  41738  hoidifhspval3  41742  hspmbllem2  41750  afveq12d  42156