Theorem ifbieq2d 4519

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-un 3913  df-if 4493

This theorem is used by:  tz7.44-2  8403  tz7.44-3  8404  oev  8508  cantnfp1lem1  9657  cantnfp1lem3  9659  ttrclselem2  9705  fin23lem12  10333  fin23lem33  10347  axcc2  10439  ttukeylem3  10513  ttukey2g  10518  canthp1lem2  10656  canthp1  10657  xnegeq  13251  xaddval  13267  xmulval  13269  expval  14119  cshfn  14853  ofccat  15032  relexpsucnnr  15088  sgnval  15151  sadcp1  16538  smupp1  16563  gcdval  16579  gcdass  16630  lcmval  16675  lcmass  16697  lcmfval  16704  lcmf0val  16705  lcmfpr  16710  iserodd  16920  pcval  16929  vdwlem6  17071  ramub1lem2  17112  ramcl  17114  mulgval  19168  symgextfv  19519  symgfixfo  19540  odfval  19633  odval  19635  submod  19670  gexval  19679  znval  21722  fvmptnn04if  23043  cpmadumatpoly  23077  cayleyhamilton  23084  cayleyhamiltonALT  23085  ptcmplem2  24247  iccpnfhmeo  25141  pcopt  25218  ioombl1  25758  ioorval  25770  uniioombllem6  25784  itg1addlem3  25894  itg2uba  25939  limcfval  26068  limcmpt  26079  limcco  26089  dvcobr  26142  ig1pval  26370  abelthlem9  26640  logtayllem  26861  logtayl  26862  leibpilem2  27143  rlimcnp2  27168  efrlim  27171  igamval  27248  muval  27333  lgsval  27502  lgsfval  27503  lgsval2lem  27508  rpvmasum2  27713  padicval  27818  padicabv  27831  expsval  28655  axlowdimlem15  29343  axlowdim  29348  eupth2lem3lem3  30618  eupth2  30627  eucrct2eupth  30633  psgnfzto1stlem  33451  sgnsv  33511  sgnsval  33512  madjusmdetlem2  34249  madjusmdet  34252  xrge0iifcv  34355  xrge0iifhom  34358  xrge0tmd  34366  xrge0tmdALT  34367  signspval  34971  ex-sategoelel  35934  rdgprc0  36304  dfrdg2  36306  dfrdg4  36464  csbrdgg  38016  finxpeq1  38073  finxpreclem3  38080  poimirlem1  38313  poimirlem7  38319  poimirlem10  38322  poimirlem11  38323  itg2addnclem  38363  itg2addnclem3  38365  itg2addnc  38366  fdc  38437  heiborlem4  38506  heiborlem6  38508  heiborlem10  38512  mapdhval  42539  hdmap1fval  42611  hdmap1vallem  42612  hdmap1val  42613  hdmap1cbv  42617  sticksstones10  42963  sticksstones12a  42965  fsuppind  43363  irrapxlem4  43593  clsk1indlem0  44808  clsk1indlem2  44809  clsk1indlem3  44810  clsk1indlem4  44811  clsk1indlem1  44812  dirkerval2  46849  dirkeritg  46857  dirkercncf  46862  fourierdlem29  46891  fourierdlem37  46899  fourierdlem62  46923  fourierdlem79  46940  fourierdlem81  46942  fourierdlem82  46943  fourierdlem92  46953  fourierdlem96  46957  fourierdlem97  46958  fourierdlem98  46959  fourierdlem99  46960  fourierdlem105  46966  fourierdlem108  46969  fourierdlem110  46971  fourierdlem112  46973  fourierdlem113  46974  fouriersw  46986  etransclem24  47013  etransclem25  47014  etransclem31  47020  etransclem35  47024  etransclem37  47026  sge0val  47121  nnfoctbdjlem  47210  nnfoctbdj  47211  ovnval  47296  ovnval2  47300  ovnval2b  47307  hsphoif  47331  hoidmvval  47332  hsphoival  47334  hoidmv1lelem1  47346  hoidmv1lelem2  47347  hoidmv1lelem3  47348  hoidmv1le  47349  ovnhoi  47358  hoidifhspval  47363  hspmbllem2  47382  ovnsubadd2  47401  blenval  49392