Theorem ifbieq2d 4406

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522  ifcif 4381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-un 3864  df-if 4382

This theorem is referenced by:  tz7.44-2  7895  tz7.44-3  7896  oev  7990  cantnfp1lem1  8987  cantnfp1lem3  8989  fin23lem12  9599  fin23lem33  9613  axcc2  9705  ttukeylem3  9779  ttukey2g  9784  canthp1lem2  9921  canthp1  9922  xnegeq  12450  xaddval  12466  xmulval  12468  expval  13281  cshfn  13988  ofccat  14163  relexpsucnnr  14218  sgnval  14281  sadcp1  15637  smupp1  15662  gcdval  15678  gcdass  15724  lcmval  15765  lcmass  15787  lcmfval  15794  lcmf0val  15795  lcmfpr  15800  iserodd  16001  pcval  16010  vdwlem6  16151  ramub1lem2  16192  ramcl  16194  mulgval  17985  symgextfv  18277  symgfixfo  18298  odfval  18391  odval  18393  submod  18424  gexval  18433  znval  20364  fvmptnn04if  21141  cpmadumatpoly  21175  cayleyhamilton  21182  cayleyhamiltonALT  21183  ptcmplem2  22345  iccpnfhmeo  23232  pcopt  23309  ioombl1  23846  ioorval  23858  uniioombllem6  23872  itg1addlem3  23982  itg2uba  24027  limcfval  24153  limcmpt  24164  limcco  24174  dvcobr  24226  ig1pval  24449  abelthlem9  24711  logtayllem  24923  logtayl  24924  leibpilem2  25201  rlimcnp2  25226  efrlim  25229  igamval  25306  muval  25391  lgsval  25559  lgsfval  25560  lgsval2lem  25565  rpvmasum2  25770  padicval  25875  padicabv  25888  axlowdimlem15  26425  axlowdim  26430  eupth2lem3lem3  27697  eupth2  27706  eucrct2eupthOLD  27713  eucrct2eupth  27714  sgnsv  30440  sgnsval  30441  psgnfzto1stlem  30664  madjusmdetlem2  30708  madjusmdet  30711  xrge0iifcv  30794  xrge0iifhom  30797  xrge0tmd  30805  xrge0tmdALT  30806  signspval  31439  ex-sategoelel  32276  rdgprc0  32647  dfrdg2  32649  dfrdg4  33021  csbrdgg  34141  finxpeq1  34198  finxpreclem3  34205  poimirlem1  34424  poimirlem7  34430  poimirlem10  34433  poimirlem11  34434  itg2addnclem  34474  itg2addnclem3  34476  itg2addnc  34477  fdc  34552  heiborlem4  34624  heiborlem6  34626  heiborlem10  34630  mapdhval  38391  hdmap1fval  38463  hdmap1vallem  38464  hdmap1val  38465  hdmap1cbv  38469  irrapxlem4  38907  clsk1indlem0  39876  clsk1indlem2  39877  clsk1indlem3  39878  clsk1indlem4  39879  clsk1indlem1  39880  dirkerval2  41921  dirkeritg  41929  dirkercncf  41934  fourierdlem29  41963  fourierdlem37  41971  fourierdlem62  41995  fourierdlem79  42012  fourierdlem81  42014  fourierdlem82  42015  fourierdlem92  42025  fourierdlem96  42029  fourierdlem97  42030  fourierdlem98  42031  fourierdlem99  42032  fourierdlem105  42038  fourierdlem108  42041  fourierdlem110  42043  fourierdlem112  42045  fourierdlem113  42046  fouriersw  42058  etransclem24  42085  etransclem25  42086  etransclem31  42092  etransclem35  42096  etransclem37  42098  sge0val  42190  nnfoctbdjlem  42279  nnfoctbdj  42280  ovnval  42365  ovnval2  42369  ovnval2b  42376  hsphoif  42400  hoidmvval  42401  hsphoival  42403  hoidmv1lelem1  42415  hoidmv1lelem2  42416  hoidmv1lelem3  42417  hoidmv1le  42418  ovnhoi  42427  hoidifhspval  42432  hspmbllem2  42451  ovnsubadd2  42470  blenval  44112