Theorem ifbieq2d 4518

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4491

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-un 3922  df-if 4492

This theorem is referenced by:  tz7.44-2  8378  tz7.44-3  8379  oev  8481  cantnfp1lem1  9638  cantnfp1lem3  9640  ttrclselem2  9686  fin23lem12  10291  fin23lem33  10305  axcc2  10397  ttukeylem3  10471  ttukey2g  10476  canthp1lem2  10613  canthp1  10614  xnegeq  13174  xaddval  13190  xmulval  13192  expval  14035  cshfn  14762  ofccat  14942  relexpsucnnr  14998  sgnval  15061  sadcp1  16432  smupp1  16457  gcdval  16473  gcdass  16524  lcmval  16569  lcmass  16591  lcmfval  16598  lcmf0val  16599  lcmfpr  16604  iserodd  16813  pcval  16822  vdwlem6  16964  ramub1lem2  17005  ramcl  17007  mulgval  19010  symgextfv  19355  symgfixfo  19376  odfval  19469  odval  19471  submod  19506  gexval  19515  znval  21452  fvmptnn04if  22743  cpmadumatpoly  22777  cayleyhamilton  22784  cayleyhamiltonALT  22785  ptcmplem2  23947  iccpnfhmeo  24850  pcopt  24929  ioombl1  25470  ioorval  25482  uniioombllem6  25496  itg1addlem3  25606  itg2uba  25651  limcfval  25780  limcmpt  25791  limcco  25801  dvcobr  25856  dvcobrOLD  25857  ig1pval  26088  abelthlem9  26357  logtayllem  26575  logtayl  26576  leibpilem2  26858  rlimcnp2  26883  efrlim  26886  efrlimOLD  26887  igamval  26964  muval  27049  lgsval  27219  lgsfval  27220  lgsval2lem  27225  rpvmasum2  27430  padicval  27535  padicabv  27548  expsval  28318  axlowdimlem15  28890  axlowdim  28895  eupth2lem3lem3  30166  eupth2  30175  eucrct2eupth  30181  psgnfzto1stlem  33064  sgnsv  33124  sgnsval  33125  madjusmdetlem2  33825  madjusmdet  33828  xrge0iifcv  33931  xrge0iifhom  33934  xrge0tmd  33942  xrge0tmdALT  33943  signspval  34550  ex-sategoelel  35415  rdgprc0  35788  dfrdg2  35790  dfrdg4  35946  csbrdgg  37324  finxpeq1  37381  finxpreclem3  37388  poimirlem1  37622  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  fdc  37746  heiborlem4  37815  heiborlem6  37817  heiborlem10  37821  mapdhval  41725  hdmap1fval  41797  hdmap1vallem  41798  hdmap1val  41799  hdmap1cbv  41803  sticksstones10  42150  sticksstones12a  42152  fsuppind  42585  irrapxlem4  42820  clsk1indlem0  44037  clsk1indlem2  44038  clsk1indlem3  44039  clsk1indlem4  44040  clsk1indlem1  44041  dirkerval2  46099  dirkeritg  46107  dirkercncf  46112  fourierdlem29  46141  fourierdlem37  46149  fourierdlem62  46173  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem92  46203  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem105  46216  fourierdlem108  46219  fourierdlem110  46221  fourierdlem112  46223  fourierdlem113  46224  fouriersw  46236  etransclem24  46263  etransclem25  46264  etransclem31  46270  etransclem35  46274  etransclem37  46276  sge0val  46371  nnfoctbdjlem  46460  nnfoctbdj  46461  ovnval  46546  ovnval2  46550  ovnval2b  46557  hsphoif  46581  hoidmvval  46582  hsphoival  46584  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmv1le  46599  ovnhoi  46608  hoidifhspval  46613  hspmbllem2  46632  ovnsubadd2  46651  blenval  48564