Theorem ifbieq2d 4506

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 4503	. 2 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3		ifbieq2d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq2d 4500	. 2 ⊢ (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
5	2, 4	eqtrd 2771	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-if 4480

This theorem is referenced by:  tz7.44-2  8338  tz7.44-3  8339  oev  8441  cantnfp1lem1  9587  cantnfp1lem3  9589  ttrclselem2  9635  fin23lem12  10241  fin23lem33  10255  axcc2  10347  ttukeylem3  10421  ttukey2g  10426  canthp1lem2  10564  canthp1  10565  xnegeq  13122  xaddval  13138  xmulval  13140  expval  13986  cshfn  14713  ofccat  14892  relexpsucnnr  14948  sgnval  15011  sadcp1  16382  smupp1  16407  gcdval  16423  gcdass  16474  lcmval  16519  lcmass  16541  lcmfval  16548  lcmf0val  16549  lcmfpr  16554  iserodd  16763  pcval  16772  vdwlem6  16914  ramub1lem2  16955  ramcl  16957  mulgval  19001  symgextfv  19347  symgfixfo  19368  odfval  19461  odval  19463  submod  19498  gexval  19507  znval  21490  fvmptnn04if  22793  cpmadumatpoly  22827  cayleyhamilton  22834  cayleyhamiltonALT  22835  ptcmplem2  23997  iccpnfhmeo  24899  pcopt  24978  ioombl1  25519  ioorval  25531  uniioombllem6  25545  itg1addlem3  25655  itg2uba  25700  limcfval  25829  limcmpt  25840  limcco  25850  dvcobr  25905  dvcobrOLD  25906  ig1pval  26137  abelthlem9  26406  logtayllem  26624  logtayl  26625  leibpilem2  26907  rlimcnp2  26932  efrlim  26935  efrlimOLD  26936  igamval  27013  muval  27098  lgsval  27268  lgsfval  27269  lgsval2lem  27274  rpvmasum2  27479  padicval  27584  padicabv  27597  expsval  28421  axlowdimlem15  29029  axlowdim  29034  eupth2lem3lem3  30305  eupth2  30314  eucrct2eupth  30320  psgnfzto1stlem  33182  sgnsv  33242  sgnsval  33243  madjusmdetlem2  33985  madjusmdet  33988  xrge0iifcv  34091  xrge0iifhom  34094  xrge0tmd  34102  xrge0tmdALT  34103  signspval  34709  ex-sategoelel  35615  rdgprc0  35985  dfrdg2  35987  dfrdg4  36145  csbrdgg  37534  finxpeq1  37591  finxpreclem3  37598  poimirlem1  37822  poimirlem7  37828  poimirlem10  37831  poimirlem11  37832  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  fdc  37946  heiborlem4  38015  heiborlem6  38017  heiborlem10  38021  mapdhval  41984  hdmap1fval  42056  hdmap1vallem  42057  hdmap1val  42058  hdmap1cbv  42062  sticksstones10  42409  sticksstones12a  42411  fsuppind  42833  irrapxlem4  43067  clsk1indlem0  44282  clsk1indlem2  44283  clsk1indlem3  44284  clsk1indlem4  44285  clsk1indlem1  44286  dirkerval2  46338  dirkeritg  46346  dirkercncf  46351  fourierdlem29  46380  fourierdlem37  46388  fourierdlem62  46412  fourierdlem79  46429  fourierdlem81  46431  fourierdlem82  46432  fourierdlem92  46442  fourierdlem96  46446  fourierdlem97  46447  fourierdlem98  46448  fourierdlem99  46449  fourierdlem105  46455  fourierdlem108  46458  fourierdlem110  46460  fourierdlem112  46462  fourierdlem113  46463  fouriersw  46475  etransclem24  46502  etransclem25  46503  etransclem31  46509  etransclem35  46513  etransclem37  46515  sge0val  46610  nnfoctbdjlem  46699  nnfoctbdj  46700  ovnval  46785  ovnval2  46789  ovnval2b  46796  hsphoif  46820  hoidmvval  46821  hsphoival  46823  hoidmv1lelem1  46835  hoidmv1lelem2  46836  hoidmv1lelem3  46837  hoidmv1le  46838  ovnhoi  46847  hoidifhspval  46852  hspmbllem2  46871  ovnsubadd2  46890  blenval  48817