Theorem ifbieq2d 4555

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-if 4530

This theorem is referenced by:  tz7.44-2  8407  tz7.44-3  8408  oev  8514  cantnfp1lem1  9673  cantnfp1lem3  9675  ttrclselem2  9721  fin23lem12  10326  fin23lem33  10340  axcc2  10432  ttukeylem3  10506  ttukey2g  10511  canthp1lem2  10648  canthp1  10649  xnegeq  13186  xaddval  13202  xmulval  13204  expval  14029  cshfn  14740  ofccat  14916  relexpsucnnr  14972  sgnval  15035  sadcp1  16396  smupp1  16421  gcdval  16437  gcdass  16489  lcmval  16529  lcmass  16551  lcmfval  16558  lcmf0val  16559  lcmfpr  16564  iserodd  16768  pcval  16777  vdwlem6  16919  ramub1lem2  16960  ramcl  16962  mulgval  18954  symgextfv  19286  symgfixfo  19307  odfval  19400  odval  19402  submod  19437  gexval  19446  znval  21087  fvmptnn04if  22351  cpmadumatpoly  22385  cayleyhamilton  22392  cayleyhamiltonALT  22393  ptcmplem2  23557  iccpnfhmeo  24461  pcopt  24538  ioombl1  25079  ioorval  25091  uniioombllem6  25105  itg1addlem3  25215  itg2uba  25261  limcfval  25389  limcmpt  25400  limcco  25410  dvcobr  25463  ig1pval  25690  abelthlem9  25952  logtayllem  26167  logtayl  26168  leibpilem2  26446  rlimcnp2  26471  efrlim  26474  igamval  26551  muval  26636  lgsval  26804  lgsfval  26805  lgsval2lem  26810  rpvmasum2  27015  padicval  27120  padicabv  27133  axlowdimlem15  28214  axlowdim  28219  eupth2lem3lem3  29483  eupth2  29492  eucrct2eupth  29498  psgnfzto1stlem  32259  sgnsv  32319  sgnsval  32320  madjusmdetlem2  32808  madjusmdet  32811  xrge0iifcv  32914  xrge0iifhom  32917  xrge0tmd  32925  xrge0tmdALT  32926  signspval  33563  ex-sategoelel  34412  rdgprc0  34765  dfrdg2  34767  dfrdg4  34923  gg-dvcobr  35176  csbrdgg  36210  finxpeq1  36267  finxpreclem3  36274  poimirlem1  36489  poimirlem7  36495  poimirlem10  36498  poimirlem11  36499  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  fdc  36613  heiborlem4  36682  heiborlem6  36684  heiborlem10  36688  mapdhval  40595  hdmap1fval  40667  hdmap1vallem  40668  hdmap1val  40669  hdmap1cbv  40673  sticksstones10  40971  sticksstones12a  40973  metakunt3  40987  metakunt4  40988  metakunt6  40990  metakunt7  40991  metakunt8  40992  metakunt10  40994  metakunt11  40995  metakunt12  40996  metakunt20  41004  metakunt21  41005  metakunt22  41006  fsuppind  41162  irrapxlem4  41563  clsk1indlem0  42792  clsk1indlem2  42793  clsk1indlem3  42794  clsk1indlem4  42795  clsk1indlem1  42796  dirkerval2  44810  dirkeritg  44818  dirkercncf  44823  fourierdlem29  44852  fourierdlem37  44860  fourierdlem62  44884  fourierdlem79  44901  fourierdlem81  44903  fourierdlem82  44904  fourierdlem92  44914  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem105  44927  fourierdlem108  44930  fourierdlem110  44932  fourierdlem112  44934  fourierdlem113  44935  fouriersw  44947  etransclem24  44974  etransclem25  44975  etransclem31  44981  etransclem35  44985  etransclem37  44987  sge0val  45082  nnfoctbdjlem  45171  nnfoctbdj  45172  ovnval  45257  ovnval2  45261  ovnval2b  45268  hsphoif  45292  hoidmvval  45293  hsphoival  45295  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmv1le  45310  ovnhoi  45319  hoidifhspval  45324  hspmbllem2  45343  ovnsubadd2  45362  blenval  47257