Theorem ifbieq2d 4493

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4466

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-if 4467

This theorem is referenced by:  tz7.44-2  8346  tz7.44-3  8347  oev  8449  cantnfp1lem1  9599  cantnfp1lem3  9601  ttrclselem2  9647  fin23lem12  10253  fin23lem33  10267  axcc2  10359  ttukeylem3  10433  ttukey2g  10438  canthp1lem2  10576  canthp1  10577  xnegeq  13159  xaddval  13175  xmulval  13177  expval  14025  cshfn  14752  ofccat  14931  relexpsucnnr  14987  sgnval  15050  sadcp1  16424  smupp1  16449  gcdval  16465  gcdass  16516  lcmval  16561  lcmass  16583  lcmfval  16590  lcmf0val  16591  lcmfpr  16596  iserodd  16806  pcval  16815  vdwlem6  16957  ramub1lem2  16998  ramcl  17000  mulgval  19047  symgextfv  19393  symgfixfo  19414  odfval  19507  odval  19509  submod  19544  gexval  19553  znval  21515  fvmptnn04if  22814  cpmadumatpoly  22848  cayleyhamilton  22855  cayleyhamiltonALT  22856  ptcmplem2  24018  iccpnfhmeo  24912  pcopt  24989  ioombl1  25529  ioorval  25541  uniioombllem6  25555  itg1addlem3  25665  itg2uba  25710  limcfval  25839  limcmpt  25850  limcco  25860  dvcobr  25913  ig1pval  26141  abelthlem9  26405  logtayllem  26623  logtayl  26624  leibpilem2  26905  rlimcnp2  26930  efrlim  26933  igamval  27010  muval  27095  lgsval  27264  lgsfval  27265  lgsval2lem  27270  rpvmasum2  27475  padicval  27580  padicabv  27593  expsval  28417  axlowdimlem15  29025  axlowdim  29030  eupth2lem3lem3  30300  eupth2  30309  eucrct2eupth  30315  psgnfzto1stlem  33161  sgnsv  33221  sgnsval  33222  madjusmdetlem2  33972  madjusmdet  33975  xrge0iifcv  34078  xrge0iifhom  34081  xrge0tmd  34089  xrge0tmdALT  34090  signspval  34696  ex-sategoelel  35603  rdgprc0  35973  dfrdg2  35975  dfrdg4  36133  csbrdgg  37645  finxpeq1  37702  finxpreclem3  37709  poimirlem1  37942  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  fdc  38066  heiborlem4  38135  heiborlem6  38137  heiborlem10  38141  mapdhval  42170  hdmap1fval  42242  hdmap1vallem  42243  hdmap1val  42244  hdmap1cbv  42248  sticksstones10  42594  sticksstones12a  42596  fsuppind  43023  irrapxlem4  43253  clsk1indlem0  44468  clsk1indlem2  44469  clsk1indlem3  44470  clsk1indlem4  44471  clsk1indlem1  44472  dirkerval2  46522  dirkeritg  46530  dirkercncf  46535  fourierdlem29  46564  fourierdlem37  46572  fourierdlem62  46596  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem92  46626  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem105  46639  fourierdlem108  46642  fourierdlem110  46644  fourierdlem112  46646  fourierdlem113  46647  fouriersw  46659  etransclem24  46686  etransclem25  46687  etransclem31  46693  etransclem35  46697  etransclem37  46699  sge0val  46794  nnfoctbdjlem  46883  nnfoctbdj  46884  ovnval  46969  ovnval2  46973  ovnval2b  46980  hsphoif  47004  hoidmvval  47005  hsphoival  47007  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmv1le  47022  ovnhoi  47031  hoidifhspval  47036  hspmbllem2  47055  ovnsubadd2  47074  blenval  49047