Theorem ifbieq2d 4508

Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypotheses

Ref	Expression
ifbieq2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq2d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifbieq2d	⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

Proof of Theorem ifbieq2d

Step	Hyp	Ref	Expression
1		ifbieq2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 4505	. 2 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3		ifbieq2d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq2d 4502	. 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:  tz7.44-2  8348  tz7.44-3  8349  oev  8451  cantnfp1lem1  9599  cantnfp1lem3  9601  ttrclselem2  9647  fin23lem12  10253  fin23lem33  10267  axcc2  10359  ttukeylem3  10433  ttukey2g  10438  canthp1lem2  10576  canthp1  10577  xnegeq  13134  xaddval  13150  xmulval  13152  expval  13998  cshfn  14725  ofccat  14904  relexpsucnnr  14960  sgnval  15023  sadcp1  16394  smupp1  16419  gcdval  16435  gcdass  16486  lcmval  16531  lcmass  16553  lcmfval  16560  lcmf0val  16561  lcmfpr  16566  iserodd  16775  pcval  16784  vdwlem6  16926  ramub1lem2  16967  ramcl  16969  mulgval  19013  symgextfv  19359  symgfixfo  19380  odfval  19473  odval  19475  submod  19510  gexval  19519  znval  21502  fvmptnn04if  22805  cpmadumatpoly  22839  cayleyhamilton  22846  cayleyhamiltonALT  22847  ptcmplem2  24009  iccpnfhmeo  24911  pcopt  24990  ioombl1  25531  ioorval  25543  uniioombllem6  25557  itg1addlem3  25667  itg2uba  25712  limcfval  25841  limcmpt  25852  limcco  25862  dvcobr  25917  dvcobrOLD  25918  ig1pval  26149  abelthlem9  26418  logtayllem  26636  logtayl  26637  leibpilem2  26919  rlimcnp2  26944  efrlim  26947  efrlimOLD  26948  igamval  27025  muval  27110  lgsval  27280  lgsfval  27281  lgsval2lem  27286  rpvmasum2  27491  padicval  27596  padicabv  27609  expsval  28433  axlowdimlem15  29041  axlowdim  29046  eupth2lem3lem3  30317  eupth2  30326  eucrct2eupth  30332  psgnfzto1stlem  33193  sgnsv  33253  sgnsval  33254  madjusmdetlem2  34005  madjusmdet  34008  xrge0iifcv  34111  xrge0iifhom  34114  xrge0tmd  34122  xrge0tmdALT  34123  signspval  34729  ex-sategoelel  35634  rdgprc0  36004  dfrdg2  36006  dfrdg4  36164  csbrdgg  37581  finxpeq1  37638  finxpreclem3  37645  poimirlem1  37869  poimirlem7  37875  poimirlem10  37878  poimirlem11  37879  itg2addnclem  37919  itg2addnclem3  37921  itg2addnc  37922  fdc  37993  heiborlem4  38062  heiborlem6  38064  heiborlem10  38068  mapdhval  42097  hdmap1fval  42169  hdmap1vallem  42170  hdmap1val  42171  hdmap1cbv  42175  sticksstones10  42522  sticksstones12a  42524  fsuppind  42945  irrapxlem4  43179  clsk1indlem0  44394  clsk1indlem2  44395  clsk1indlem3  44396  clsk1indlem4  44397  clsk1indlem1  44398  dirkerval2  46449  dirkeritg  46457  dirkercncf  46462  fourierdlem29  46491  fourierdlem37  46499  fourierdlem62  46523  fourierdlem79  46540  fourierdlem81  46542  fourierdlem82  46543  fourierdlem92  46553  fourierdlem96  46557  fourierdlem97  46558  fourierdlem98  46559  fourierdlem99  46560  fourierdlem105  46566  fourierdlem108  46569  fourierdlem110  46571  fourierdlem112  46573  fourierdlem113  46574  fouriersw  46586  etransclem24  46613  etransclem25  46614  etransclem31  46620  etransclem35  46624  etransclem37  46626  sge0val  46721  nnfoctbdjlem  46810  nnfoctbdj  46811  ovnval  46896  ovnval2  46900  ovnval2b  46907  hsphoif  46931  hoidmvval  46932  hsphoival  46934  hoidmv1lelem1  46946  hoidmv1lelem2  46947  hoidmv1lelem3  46948  hoidmv1le  46949  ovnhoi  46958  hoidifhspval  46963  hspmbllem2  46982  ovnsubadd2  47001  blenval  48928