Theorem ifbieq2d 4509

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-if 4483

This theorem is used by:  tz7.44-2  8408  tz7.44-3  8409  oev  8515  cantnfp1lem1  9672  cantnfp1lem3  9674  ttrclselem2  9720  fin23lem12  10402  fin23lem33  10416  axcc2  10508  ttukeylem3  10582  ttukey2g  10587  canthp1lem2  10731  canthp1  10732  xnegeq  13330  xaddval  13346  xmulval  13348  expval  14199  cshfn  14934  ofccat  15115  relexpsucnnr  15171  sgnval  15234  sadcp1  16618  smupp1  16643  gcdval  16659  gcdass  16713  lcmval  16760  lcmass  16782  lcmfval  16789  lcmf0val  16790  lcmfpr  16795  iserodd  17006  pcval  17015  vdwlem6  17157  ramub1lem2  17198  ramcl  17200  mulgval  19274  symgextfv  19625  symgfixfo  19646  odfval  19739  odval  19741  submod  19776  gexval  19785  znval  21834  fvmptnn04if  23160  cpmadumatpoly  23194  cayleyhamilton  23201  cayleyhamiltonALT  23202  ptcmplem2  24365  iccpnfhmeo  25259  pcopt  25336  ioombl1  25876  ioorval  25888  uniioombllem6  25902  itg1addlem3  26012  itg2uba  26057  limcfval  26185  limcmpt  26196  limcco  26206  dvcobr  26259  ig1pval  26487  abelthlem9  26760  logtayllem  26980  logtayl  26981  leibpilem2  27262  rlimcnp2  27287  efrlim  27290  igamval  27367  muval  27452  lgsval  27621  lgsfval  27622  lgsval2lem  27627  rpvmasum2  27832  padicval  27937  padicabv  27950  expsval  28804  axlowdimlem15  29527  axlowdim  29532  eupth2lem3lem3  30824  eupth2  30833  eucrct2eupth  30839  psgnfzto1stlem  33654  sgnsv  33714  sgnsval  33715  madjusmdetlem2  34453  madjusmdet  34456  xrge0iifcv  34559  xrge0iifhom  34562  xrge0tmd  34570  xrge0tmdALT  34571  signspval  35174  ex-sategoelel  36165  rdgprc0  36535  dfrdg2  36537  dfrdg4  36695  csbrdgg  38232  finxpeq1  38289  finxpreclem3  38296  poimirlem1  38519  poimirlem7  38525  poimirlem10  38528  poimirlem11  38529  itg2addnclem  38569  itg2addnclem3  38571  itg2addnc  38572  fdc  38659  heiborlem4  38728  heiborlem6  38730  heiborlem10  38734  mapdhval  42761  hdmap1fval  42833  hdmap1vallem  42834  hdmap1val  42835  hdmap1cbv  42839  sticksstones10  43185  sticksstones12a  43187  fsuppind  43598  irrapxlem4  43811  clsk1indlem0  45026  clsk1indlem2  45027  clsk1indlem3  45028  clsk1indlem4  45029  clsk1indlem1  45030  dirkerval2  47073  dirkeritg  47081  dirkercncf  47086  fourierdlem29  47115  fourierdlem37  47123  fourierdlem62  47147  fourierdlem79  47164  fourierdlem81  47166  fourierdlem82  47167  fourierdlem92  47177  fourierdlem96  47181  fourierdlem97  47182  fourierdlem98  47183  fourierdlem99  47184  fourierdlem105  47190  fourierdlem108  47193  fourierdlem110  47195  fourierdlem112  47197  fourierdlem113  47198  fouriersw  47210  etransclem24  47237  etransclem25  47238  etransclem31  47244  etransclem35  47248  etransclem37  47250  sge0val  47345  nnfoctbdjlem  47434  nnfoctbdj  47435  ovnval  47520  ovnval2  47524  ovnval2b  47531  hsphoif  47555  hoidmvval  47556  hsphoival  47558  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmv1lelem3  47572  hoidmv1le  47573  ovnhoi  47582  hoidifhspval  47587  hspmbllem2  47606  ovnsubadd2  47625  blenval  49652