Theorem ifbieq2d 4503

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ifcif 4477

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3444  df-un 3906  df-if 4478

This theorem is referenced by:  tz7.44-2  8312  tz7.44-3  8313  oev  8419  cantnfp1lem1  9539  cantnfp1lem3  9541  ttrclselem2  9587  fin23lem12  10192  fin23lem33  10206  axcc2  10298  ttukeylem3  10372  ttukey2g  10377  canthp1lem2  10514  canthp1  10515  xnegeq  13046  xaddval  13062  xmulval  13064  expval  13889  cshfn  14601  ofccat  14779  relexpsucnnr  14835  sgnval  14898  sadcp1  16261  smupp1  16286  gcdval  16302  gcdass  16354  lcmval  16394  lcmass  16416  lcmfval  16423  lcmf0val  16424  lcmfpr  16429  iserodd  16633  pcval  16642  vdwlem6  16784  ramub1lem2  16825  ramcl  16827  mulgval  18800  symgextfv  19122  symgfixfo  19143  odfval  19236  odval  19238  submod  19270  gexval  19279  znval  20844  fvmptnn04if  22103  cpmadumatpoly  22137  cayleyhamilton  22144  cayleyhamiltonALT  22145  ptcmplem2  23309  iccpnfhmeo  24213  pcopt  24290  ioombl1  24831  ioorval  24843  uniioombllem6  24857  itg1addlem3  24967  itg2uba  25013  limcfval  25141  limcmpt  25152  limcco  25162  dvcobr  25215  ig1pval  25442  abelthlem9  25704  logtayllem  25919  logtayl  25920  leibpilem2  26196  rlimcnp2  26221  efrlim  26224  igamval  26301  muval  26386  lgsval  26554  lgsfval  26555  lgsval2lem  26560  rpvmasum2  26765  padicval  26870  padicabv  26883  axlowdimlem15  27612  axlowdim  27617  eupth2lem3lem3  28881  eupth2  28890  eucrct2eupth  28896  psgnfzto1stlem  31652  sgnsv  31712  sgnsval  31713  madjusmdetlem2  32074  madjusmdet  32077  xrge0iifcv  32180  xrge0iifhom  32183  xrge0tmd  32191  xrge0tmdALT  32192  signspval  32829  ex-sategoelel  33680  rdgprc0  34052  dfrdg2  34054  dfrdg4  34390  csbrdgg  35654  finxpeq1  35711  finxpreclem3  35718  poimirlem1  35934  poimirlem7  35940  poimirlem10  35943  poimirlem11  35944  itg2addnclem  35984  itg2addnclem3  35986  itg2addnc  35987  fdc  36059  heiborlem4  36128  heiborlem6  36130  heiborlem10  36134  mapdhval  40043  hdmap1fval  40115  hdmap1vallem  40116  hdmap1val  40117  hdmap1cbv  40121  sticksstones10  40419  sticksstones12a  40421  metakunt3  40435  metakunt4  40436  metakunt6  40438  metakunt7  40439  metakunt8  40440  metakunt10  40442  metakunt11  40443  metakunt12  40444  metakunt20  40452  metakunt21  40453  metakunt22  40454  fsuppind  40590  irrapxlem4  40960  clsk1indlem0  42024  clsk1indlem2  42025  clsk1indlem3  42026  clsk1indlem4  42027  clsk1indlem1  42028  dirkerval2  44023  dirkeritg  44031  dirkercncf  44036  fourierdlem29  44065  fourierdlem37  44073  fourierdlem62  44097  fourierdlem79  44114  fourierdlem81  44116  fourierdlem82  44117  fourierdlem92  44127  fourierdlem96  44131  fourierdlem97  44132  fourierdlem98  44133  fourierdlem99  44134  fourierdlem105  44140  fourierdlem108  44143  fourierdlem110  44145  fourierdlem112  44147  fourierdlem113  44148  fouriersw  44160  etransclem24  44187  etransclem25  44188  etransclem31  44194  etransclem35  44198  etransclem37  44200  sge0val  44293  nnfoctbdjlem  44382  nnfoctbdj  44383  ovnval  44468  ovnval2  44472  ovnval2b  44479  hsphoif  44503  hoidmvval  44504  hsphoival  44506  hoidmv1lelem1  44518  hoidmv1lelem2  44519  hoidmv1lelem3  44520  hoidmv1le  44521  ovnhoi  44530  hoidifhspval  44535  hspmbllem2  44554  ovnsubadd2  44573  blenval  46335