Theorem ifbieq1d 4493

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536  ifcif 4470

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-un 3944  df-if 4471

This theorem is referenced by:  opeq1  4806  opeq2  4807  oieq1  8979  oieq2  8980  cantnflem1d  9154  cantnflem1  9155  iunfictbso  9543  ttukey2g  9941  bcval  13667  swrdval  14008  summolem2a  15075  zsum  15078  fsum  15080  sumss  15084  sumss2  15086  fsumcvg2  15087  fsumser  15090  isumless  15203  cbvprod  15272  prodmolem2a  15291  zprod  15294  fprod  15298  fprodntriv  15299  prodss  15304  rpnnen2lem1  15570  sadadd2lem  15811  sadadd2  15812  pcmpt  16231  pcmptdvds  16233  prmreclem2  16256  prmreclem4  16258  prmreclem5  16259  prmreclem6  16260  prmrec  16261  ramub1lem2  16366  ramcl  16368  prmop1  16377  prmonn2  16378  prmdvdsprmo  16381  fvprmselelfz  16383  fvprmselgcd1  16384  prmodvdslcmf  16386  prmgapprmo  16401  smndex2dlinvh  18085  pmtrval  18582  pmtrdifellem3  18609  cyggenod2  19007  gsummpt1n0  19088  dmdprdsplitlem  19162  cycsubggenodd  19234  evlslem2  20295  coe1tmmul2fv  20449  coe1pwmulfv  20451  cyggic  20722  dmatmulcl  21112  scmatscmiddistr  21120  marrepval  21174  maducoeval  21251  maducoeval2  21252  minmar1val  21260  fclsval  22619  stdbdmetval  23127  stdbdxmet  23128  pcopt2  23630  cmetcaulem  23894  ovolicc2lem3  24123  ovolicc2lem4  24124  ovolicc2lem5  24125  mbfposb  24257  i1fres  24309  i1fposd  24311  mbfi1fseqlem2  24320  mbfi1fseq  24325  mbfi1flimlem  24326  mbfi1flim  24327  itg2splitlem  24352  itg2cnlem1  24365  itg2cn  24367  isibl  24369  isibl2  24370  iblitg  24372  dfitg  24373  cbvitg  24379  itgeq2  24381  itgvallem  24388  iblneg  24406  itgneg  24407  itgss3  24418  itgcn  24446  deg1suble  24704  elply2  24789  dgrsub  24865  aareccl  24918  vmaval  25693  prmorcht  25758  pclogsum  25794  dchrelbasd  25818  dchrptlem2  25844  bposlem5  25867  lgsfval  25881  lgsdir  25911  lgsdilem2  25912  lgsdi  25913  lgsne0  25914  rplogsumlem2  26064  pntrlog2bndlem4  26159  pntrlog2bndlem5  26160  ballotlemsval  31770  ballotlemieq  31778  mrsubfval  32759  poimirlem1  34897  poimirlem5  34901  poimirlem6  34902  poimirlem12  34908  poimirlem22  34918  mblfinlem2  34934  itg2addnclem  34947  ftc1anclem5  34975  ftc1anclem6  34976  cdlemk40  38057  dvnprodlem1  42237  fourierdlem86  42484  fourierdlem97  42495  fourierdlem103  42501  fourierdlem104  42502  fourierdlem112  42510  isomennd  42820  hsphoif  42865  hsphoival  42868  sge0hsphoire  42878  hoidmv1lelem2  42881  hoidmv1lelem3  42882  hoidmv1le  42883  hoidmvlelem1  42884  hoidmvlelem2  42885  hoidmvlelem3  42886  hoidmvlelem4  42887  hoidmvlelem5  42888  hspval  42898  hoidifhspval2  42904  hoidifhspval3  42908  hspmbllem2  42916  afveq12d  43339