Theorem ifbieq2d 4482

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-if 4457

This theorem is referenced by:  tz7.44-2  8209  tz7.44-3  8210  oev  8306  cantnfp1lem1  9366  cantnfp1lem3  9368  fin23lem12  10018  fin23lem33  10032  axcc2  10124  ttukeylem3  10198  ttukey2g  10203  canthp1lem2  10340  canthp1  10341  xnegeq  12870  xaddval  12886  xmulval  12888  expval  13712  cshfn  14431  ofccat  14608  relexpsucnnr  14664  sgnval  14727  sadcp1  16090  smupp1  16115  gcdval  16131  gcdass  16183  lcmval  16225  lcmass  16247  lcmfval  16254  lcmf0val  16255  lcmfpr  16260  iserodd  16464  pcval  16473  vdwlem6  16615  ramub1lem2  16656  ramcl  16658  mulgval  18619  symgextfv  18941  symgfixfo  18962  odfval  19055  odval  19057  submod  19089  gexval  19098  znval  20651  fvmptnn04if  21906  cpmadumatpoly  21940  cayleyhamilton  21947  cayleyhamiltonALT  21948  ptcmplem2  23112  iccpnfhmeo  24014  pcopt  24091  ioombl1  24631  ioorval  24643  uniioombllem6  24657  itg1addlem3  24767  itg2uba  24813  limcfval  24941  limcmpt  24952  limcco  24962  dvcobr  25015  ig1pval  25242  abelthlem9  25504  logtayllem  25719  logtayl  25720  leibpilem2  25996  rlimcnp2  26021  efrlim  26024  igamval  26101  muval  26186  lgsval  26354  lgsfval  26355  lgsval2lem  26360  rpvmasum2  26565  padicval  26670  padicabv  26683  axlowdimlem15  27227  axlowdim  27232  eupth2lem3lem3  28495  eupth2  28504  eucrct2eupth  28510  psgnfzto1stlem  31269  sgnsv  31329  sgnsval  31330  madjusmdetlem2  31680  madjusmdet  31683  xrge0iifcv  31786  xrge0iifhom  31789  xrge0tmd  31797  xrge0tmdALT  31798  signspval  32431  ex-sategoelel  33283  rdgprc0  33675  dfrdg2  33677  ttrclselem2  33712  dfrdg4  34180  csbrdgg  35427  finxpeq1  35484  finxpreclem3  35491  poimirlem1  35705  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  fdc  35830  heiborlem4  35899  heiborlem6  35901  heiborlem10  35905  mapdhval  39665  hdmap1fval  39737  hdmap1vallem  39738  hdmap1val  39739  hdmap1cbv  39743  sticksstones10  40039  sticksstones12a  40041  metakunt3  40055  metakunt4  40056  metakunt6  40058  metakunt7  40059  metakunt8  40060  metakunt10  40062  metakunt11  40063  metakunt12  40064  metakunt20  40072  metakunt21  40073  metakunt22  40074  fsuppind  40202  irrapxlem4  40563  clsk1indlem0  41540  clsk1indlem2  41541  clsk1indlem3  41542  clsk1indlem4  41543  clsk1indlem1  41544  dirkerval2  43525  dirkeritg  43533  dirkercncf  43538  fourierdlem29  43567  fourierdlem37  43575  fourierdlem62  43599  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem92  43629  fourierdlem96  43633  fourierdlem97  43634  fourierdlem98  43635  fourierdlem99  43636  fourierdlem105  43642  fourierdlem108  43645  fourierdlem110  43647  fourierdlem112  43649  fourierdlem113  43650  fouriersw  43662  etransclem24  43689  etransclem25  43690  etransclem31  43696  etransclem35  43700  etransclem37  43702  sge0val  43794  nnfoctbdjlem  43883  nnfoctbdj  43884  ovnval  43969  ovnval2  43973  ovnval2b  43980  hsphoif  44004  hoidmvval  44005  hsphoival  44007  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmv1le  44022  ovnhoi  44031  hoidifhspval  44036  hspmbllem2  44055  ovnsubadd2  44074  blenval  45805