Theorem ifbieq2d 4492

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-un 3941  df-if 4468

This theorem is referenced by:  tz7.44-2  8043  tz7.44-3  8044  oev  8139  cantnfp1lem1  9141  cantnfp1lem3  9143  fin23lem12  9753  fin23lem33  9767  axcc2  9859  ttukeylem3  9933  ttukey2g  9938  canthp1lem2  10075  canthp1  10076  xnegeq  12601  xaddval  12617  xmulval  12619  expval  13432  cshfn  14152  ofccat  14329  relexpsucnnr  14384  sgnval  14447  sadcp1  15804  smupp1  15829  gcdval  15845  gcdass  15895  lcmval  15936  lcmass  15958  lcmfval  15965  lcmf0val  15966  lcmfpr  15971  iserodd  16172  pcval  16181  vdwlem6  16322  ramub1lem2  16363  ramcl  16365  mulgval  18228  symgextfv  18546  symgfixfo  18567  odfval  18660  odval  18662  submod  18694  gexval  18703  znval  20682  fvmptnn04if  21457  cpmadumatpoly  21491  cayleyhamilton  21498  cayleyhamiltonALT  21499  ptcmplem2  22661  iccpnfhmeo  23549  pcopt  23626  ioombl1  24163  ioorval  24175  uniioombllem6  24189  itg1addlem3  24299  itg2uba  24344  limcfval  24470  limcmpt  24481  limcco  24491  dvcobr  24543  ig1pval  24766  abelthlem9  25028  logtayllem  25242  logtayl  25243  leibpilem2  25519  rlimcnp2  25544  efrlim  25547  igamval  25624  muval  25709  lgsval  25877  lgsfval  25878  lgsval2lem  25883  rpvmasum2  26088  padicval  26193  padicabv  26206  axlowdimlem15  26742  axlowdim  26747  eupth2lem3lem3  28009  eupth2  28018  eucrct2eupth  28024  psgnfzto1stlem  30742  sgnsv  30802  sgnsval  30803  madjusmdetlem2  31093  madjusmdet  31096  xrge0iifcv  31177  xrge0iifhom  31180  xrge0tmd  31188  xrge0tmdALT  31189  signspval  31822  ex-sategoelel  32668  rdgprc0  33038  dfrdg2  33040  dfrdg4  33412  csbrdgg  34613  finxpeq1  34670  finxpreclem3  34677  poimirlem1  34908  poimirlem7  34914  poimirlem10  34917  poimirlem11  34918  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  fdc  35035  heiborlem4  35107  heiborlem6  35109  heiborlem10  35113  mapdhval  38875  hdmap1fval  38947  hdmap1vallem  38948  hdmap1val  38949  hdmap1cbv  38953  irrapxlem4  39471  clsk1indlem0  40440  clsk1indlem2  40441  clsk1indlem3  40442  clsk1indlem4  40443  clsk1indlem1  40444  dirkerval2  42428  dirkeritg  42436  dirkercncf  42441  fourierdlem29  42470  fourierdlem37  42478  fourierdlem62  42502  fourierdlem79  42519  fourierdlem81  42521  fourierdlem82  42522  fourierdlem92  42532  fourierdlem96  42536  fourierdlem97  42537  fourierdlem98  42538  fourierdlem99  42539  fourierdlem105  42545  fourierdlem108  42548  fourierdlem110  42550  fourierdlem112  42552  fourierdlem113  42553  fouriersw  42565  etransclem24  42592  etransclem25  42593  etransclem31  42599  etransclem35  42603  etransclem37  42605  sge0val  42697  nnfoctbdjlem  42786  nnfoctbdj  42787  ovnval  42872  ovnval2  42876  ovnval2b  42883  hsphoif  42907  hoidmvval  42908  hsphoival  42910  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmv1le  42925  ovnhoi  42934  hoidifhspval  42939  hspmbllem2  42958  ovnsubadd2  42977  blenval  44680