Theorem ifbieq1d 4506

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-un 3908  df-if 4482

This theorem is referenced by:  opeq1  4831  opeq2  4832  oieq1  9429  oieq2  9430  cantnflem1d  9609  cantnflem1  9610  ttrcltr  9637  iunfictbso  10036  ttukey2g  10438  bcval  14239  swrdval  14579  summolem2a  15650  zsum  15653  fsum  15655  sumss  15659  sumss2  15661  fsumcvg2  15662  fsumser  15665  isumless  15780  cbvprod  15848  cbvprodv  15849  prodmolem2a  15869  zprod  15872  fprod  15876  fprodntriv  15877  prodss  15882  rpnnen2lem1  16151  sadadd2lem  16398  sadadd2  16399  pcmpt  16832  pcmptdvds  16834  prmreclem2  16857  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  prmrec  16862  ramub1lem2  16967  ramcl  16969  prmop1  16978  prmonn2  16979  prmdvdsprmo  16982  fvprmselelfz  16984  fvprmselgcd1  16985  prmodvdslcmf  16987  prmgapprmo  17002  smndex2dlinvh  18854  pmtrval  19392  pmtrdifellem3  19419  cyggenod2  19826  gsummpt1n0  19906  dmdprdsplitlem  19980  cycsubggenodd  20052  cyggic  21539  evlslem2  22046  coe1tmmul2fv  22232  coe1pwmulfv  22234  dmatmulcl  22456  scmatscmiddistr  22464  marrepval  22518  maducoeval  22595  maducoeval2  22596  minmar1val  22604  fclsval  23964  stdbdmetval  24470  stdbdxmet  24471  pcopt2  24991  cmetcaulem  25256  ovolicc2lem3  25488  ovolicc2lem4  25489  ovolicc2lem5  25490  mbfposb  25622  i1fres  25674  i1fposd  25676  mbfi1fseqlem2  25685  mbfi1fseq  25690  mbfi1flimlem  25691  mbfi1flim  25692  itg2splitlem  25717  itg2cnlem1  25730  itg2cn  25732  isibl  25734  isibl2  25735  iblitg  25737  dfitg  25738  cbvitg  25745  itgeq2  25747  itgvallem  25754  iblneg  25772  itgneg  25773  itgss3  25784  itgcn  25814  deg1suble  26080  elply2  26169  dgrsub  26246  aareccl  26302  vmaval  27091  prmorcht  27156  pclogsum  27194  dchrelbasd  27218  dchrptlem2  27244  bposlem5  27267  lgsfval  27281  lgsdir  27311  lgsdilem2  27312  lgsdi  27313  lgsne0  27314  rplogsumlem2  27464  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  elrspunsn  33521  gsummoncoe1fzo  33689  extvfval  33708  extvfvv  33710  fldextrspunlsp  33851  extdgfialglem2  33870  ballotlemsval  34686  ballotlemieq  34694  mrsubfval  35721  cbvprodvw2  36460  cbvproddavw  36493  cbvsumdavw2  36508  cbvproddavw2  36509  poimirlem1  37866  poimirlem5  37870  poimirlem6  37871  poimirlem12  37877  poimirlem22  37887  mblfinlem2  37903  itg2addnclem  37916  ftc1anclem5  37942  ftc1anclem6  37943  cdlemk40  41287  fsuppind  42942  cantnfub  43672  dvnprodlem1  46298  fourierdlem86  46544  fourierdlem97  46555  fourierdlem103  46561  fourierdlem104  46562  fourierdlem112  46570  isomennd  46883  hsphoif  46928  hsphoival  46931  sge0hsphoire  46941  hoidmv1lelem2  46944  hoidmv1lelem3  46945  hoidmv1le  46946  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem4  46950  hoidmvlelem5  46951  hspval  46961  hoidifhspval2  46967  hoidifhspval3  46971  hspmbllem2  46979  afveq12d  47487  discsubc  49417  oppfvalg  49479