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 2795	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 4151  df-if 4482

This theorem is used by:  tz7.44-2  8419  tz7.44-3  8420  oev  8526  cantnfp1lem1  9683  cantnfp1lem3  9685  ttrclselem2  9731  fin23lem12  10413  fin23lem33  10427  axcc2  10519  ttukeylem3  10593  ttukey2g  10598  canthp1lem2  10742  canthp1  10743  xnegeq  13341  xaddval  13357  xmulval  13359  expval  14210  cshfn  14946  ofccat  15128  relexpsucnnr  15184  sgnval  15247  sadcp1  16631  smupp1  16656  gcdval  16672  gcdass  16726  lcmval  16773  lcmass  16795  lcmfval  16802  lcmf0val  16803  lcmfpr  16808  iserodd  17019  pcval  17028  vdwlem6  17170  ramub1lem2  17211  ramcl  17213  mulgval  19287  symgextfv  19638  symgfixfo  19659  odfval  19752  odval  19754  submod  19789  gexval  19798  znval  21847  fvmptnn04if  23173  cpmadumatpoly  23207  cayleyhamilton  23214  cayleyhamiltonALT  23215  ptcmplem2  24378  iccpnfhmeo  25272  pcopt  25349  ioombl1  25889  ioorval  25901  uniioombllem6  25915  itg1addlem3  26025  itg2uba  26070  limcfval  26198  limcmpt  26209  limcco  26219  dvcobr  26272  ig1pval  26500  abelthlem9  26773  logtayllem  26993  logtayl  26994  leibpilem2  27275  rlimcnp2  27300  efrlim  27303  igamval  27380  muval  27465  lgsval  27634  lgsfval  27635  lgsval2lem  27640  rpvmasum2  27845  padicval  27950  padicabv  27963  expsval  28817  axlowdimlem15  29540  axlowdim  29545  eupth2lem3lem3  30837  eupth2  30846  eucrct2eupth  30852  psgnfzto1stlem  33708  sgnsv  33768  sgnsval  33769  madjusmdetlem2  34507  madjusmdet  34510  xrge0iifcv  34613  xrge0iifhom  34616  xrge0tmd  34624  xrge0tmdALT  34625  signspval  35228  ex-sategoelel  36273  rdgprc0  36648  dfrdg2  36650  dfrdg4  36808  csbrdgg  38346  finxpeq1  38403  finxpreclem3  38410  poimirlem1  38633  poimirlem7  38639  poimirlem10  38642  poimirlem11  38643  itg2addnclem  38683  itg2addnclem3  38685  itg2addnc  38686  fdc  38773  heiborlem4  38842  heiborlem6  38844  heiborlem10  38848  mapdhval  42875  hdmap1fval  42947  hdmap1vallem  42948  hdmap1val  42949  hdmap1cbv  42953  sticksstones10  43299  sticksstones12a  43301  fsuppind  43712  irrapxlem4  43926  clsk1indlem0  45135  clsk1indlem2  45136  clsk1indlem3  45137  clsk1indlem4  45138  clsk1indlem1  45139  dirkerval2  47198  dirkeritg  47206  dirkercncf  47211  fourierdlem29  47240  fourierdlem37  47248  fourierdlem62  47272  fourierdlem79  47289  fourierdlem81  47291  fourierdlem82  47292  fourierdlem92  47302  fourierdlem96  47306  fourierdlem97  47307  fourierdlem98  47308  fourierdlem99  47309  fourierdlem105  47315  fourierdlem108  47318  fourierdlem110  47320  fourierdlem112  47322  fourierdlem113  47323  fouriersw  47335  etransclem24  47362  etransclem25  47363  etransclem31  47369  etransclem35  47373  etransclem37  47375  sge0val  47470  nnfoctbdjlem  47559  nnfoctbdj  47560  ovnval  47645  ovnval2  47649  ovnval2b  47656  hsphoif  47680  hoidmvval  47681  hsphoival  47683  hoidmv1lelem1  47695  hoidmv1lelem2  47696  hoidmv1lelem3  47697  hoidmv1le  47698  ovnhoi  47707  hoidifhspval  47712  hspmbllem2  47731  ovnsubadd2  47750  blenval  49777  parhomval  50837  parhomvaln0  50847  parswapval  50870