Theorem ifbieq2d 4559

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  ifcif 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-un 3952  df-if 4534

This theorem is referenced by:  tz7.44-2  8437  tz7.44-3  8438  oev  8544  cantnfp1lem1  9721  cantnfp1lem3  9723  ttrclselem2  9769  fin23lem12  10374  fin23lem33  10388  axcc2  10480  ttukeylem3  10554  ttukey2g  10559  canthp1lem2  10696  canthp1  10697  xnegeq  13240  xaddval  13256  xmulval  13258  expval  14083  cshfn  14798  ofccat  14974  relexpsucnnr  15030  sgnval  15093  sadcp1  16455  smupp1  16480  gcdval  16496  gcdass  16548  lcmval  16593  lcmass  16615  lcmfval  16622  lcmf0val  16623  lcmfpr  16628  iserodd  16837  pcval  16846  vdwlem6  16988  ramub1lem2  17029  ramcl  17031  mulgval  19065  symgextfv  19416  symgfixfo  19437  odfval  19530  odval  19532  submod  19567  gexval  19576  znval  21529  fvmptnn04if  22842  cpmadumatpoly  22876  cayleyhamilton  22883  cayleyhamiltonALT  22884  ptcmplem2  24048  iccpnfhmeo  24961  pcopt  25040  ioombl1  25582  ioorval  25594  uniioombllem6  25608  itg1addlem3  25718  itg2uba  25764  limcfval  25892  limcmpt  25903  limcco  25913  dvcobr  25968  dvcobrOLD  25969  ig1pval  26203  abelthlem9  26470  logtayllem  26686  logtayl  26687  leibpilem2  26969  rlimcnp2  26994  efrlim  26997  efrlimOLD  26998  igamval  27075  muval  27160  lgsval  27330  lgsfval  27331  lgsval2lem  27336  rpvmasum2  27541  padicval  27646  padicabv  27659  axlowdimlem15  28890  axlowdim  28895  eupth2lem3lem3  30163  eupth2  30172  eucrct2eupth  30178  psgnfzto1stlem  32978  sgnsv  33038  sgnsval  33039  madjusmdetlem2  33643  madjusmdet  33646  xrge0iifcv  33749  xrge0iifhom  33752  xrge0tmd  33760  xrge0tmdALT  33761  signspval  34398  ex-sategoelel  35249  rdgprc0  35617  dfrdg2  35619  dfrdg4  35775  csbrdgg  37036  finxpeq1  37093  finxpreclem3  37100  poimirlem1  37322  poimirlem7  37328  poimirlem10  37331  poimirlem11  37332  itg2addnclem  37372  itg2addnclem3  37374  itg2addnc  37375  fdc  37446  heiborlem4  37515  heiborlem6  37517  heiborlem10  37521  mapdhval  41423  hdmap1fval  41495  hdmap1vallem  41496  hdmap1val  41497  hdmap1cbv  41501  sticksstones10  41853  sticksstones12a  41855  metakunt3  41893  metakunt4  41894  metakunt6  41896  metakunt7  41897  metakunt8  41898  metakunt10  41900  metakunt11  41901  metakunt12  41902  metakunt20  41910  metakunt21  41911  metakunt22  41912  fsuppind  42062  irrapxlem4  42482  clsk1indlem0  43708  clsk1indlem2  43709  clsk1indlem3  43710  clsk1indlem4  43711  clsk1indlem1  43712  dirkerval2  45715  dirkeritg  45723  dirkercncf  45728  fourierdlem29  45757  fourierdlem37  45765  fourierdlem62  45789  fourierdlem79  45806  fourierdlem81  45808  fourierdlem82  45809  fourierdlem92  45819  fourierdlem96  45823  fourierdlem97  45824  fourierdlem98  45825  fourierdlem99  45826  fourierdlem105  45832  fourierdlem108  45835  fourierdlem110  45837  fourierdlem112  45839  fourierdlem113  45840  fouriersw  45852  etransclem24  45879  etransclem25  45880  etransclem31  45886  etransclem35  45890  etransclem37  45892  sge0val  45987  nnfoctbdjlem  46076  nnfoctbdj  46077  ovnval  46162  ovnval2  46166  ovnval2b  46173  hsphoif  46197  hoidmvval  46198  hsphoival  46200  hoidmv1lelem1  46212  hoidmv1lelem2  46213  hoidmv1lelem3  46214  hoidmv1le  46215  ovnhoi  46224  hoidifhspval  46229  hspmbllem2  46248  ovnsubadd2  46267  blenval  47959