Theorem ifbieq2d 4510

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-un 3912  df-if 4484

This theorem is referenced by:  tz7.44-2  8382  tz7.44-3  8383  oev  8487  cantnfp1lem1  9635  cantnfp1lem3  9637  ttrclselem2  9683  fin23lem12  10303  fin23lem33  10317  axcc2  10409  ttukeylem3  10483  ttukey2g  10488  canthp1lem2  10626  canthp1  10627  xnegeq  13221  xaddval  13237  xmulval  13239  expval  14087  cshfn  14815  ofccat  14994  relexpsucnnr  15050  sgnval  15113  sadcp1  16501  smupp1  16526  gcdval  16542  gcdass  16593  lcmval  16638  lcmass  16660  lcmfval  16667  lcmf0val  16668  lcmfpr  16673  iserodd  16883  pcval  16892  vdwlem6  17034  ramub1lem2  17075  ramcl  17077  mulgval  19125  symgextfv  19476  symgfixfo  19497  odfval  19590  odval  19592  submod  19627  gexval  19636  znval  21642  fvmptnn04if  22963  cpmadumatpoly  22997  cayleyhamilton  23004  cayleyhamiltonALT  23005  ptcmplem2  24167  iccpnfhmeo  25061  pcopt  25138  ioombl1  25678  ioorval  25690  uniioombllem6  25704  itg1addlem3  25814  itg2uba  25859  limcfval  25988  limcmpt  25999  limcco  26009  dvcobr  26062  ig1pval  26290  abelthlem9  26557  logtayllem  26778  logtayl  26779  leibpilem2  27060  rlimcnp2  27085  efrlim  27088  igamval  27165  muval  27250  lgsval  27419  lgsfval  27420  lgsval2lem  27425  rpvmasum2  27630  padicval  27735  padicabv  27748  expsval  28572  axlowdimlem15  29211  axlowdim  29216  eupth2lem3lem3  30486  eupth2  30495  eucrct2eupth  30501  psgnfzto1stlem  33328  sgnsv  33388  sgnsval  33389  madjusmdetlem2  34130  madjusmdet  34133  xrge0iifcv  34236  xrge0iifhom  34239  xrge0tmd  34247  xrge0tmdALT  34248  signspval  34851  ex-sategoelel  35779  rdgprc0  36149  dfrdg2  36151  dfrdg4  36309  csbrdgg  37830  finxpeq1  37887  finxpreclem3  37894  poimirlem1  38127  poimirlem7  38133  poimirlem10  38136  poimirlem11  38137  itg2addnclem  38177  itg2addnclem3  38179  itg2addnc  38180  fdc  38251  heiborlem4  38320  heiborlem6  38322  heiborlem10  38326  mapdhval  42355  hdmap1fval  42427  hdmap1vallem  42428  hdmap1val  42429  hdmap1cbv  42433  sticksstones10  42779  sticksstones12a  42781  fsuppind  43179  irrapxlem4  43409  clsk1indlem0  44624  clsk1indlem2  44625  clsk1indlem3  44626  clsk1indlem4  44627  clsk1indlem1  44628  dirkerval2  46667  dirkeritg  46675  dirkercncf  46680  fourierdlem29  46709  fourierdlem37  46717  fourierdlem62  46741  fourierdlem79  46758  fourierdlem81  46760  fourierdlem82  46761  fourierdlem92  46771  fourierdlem96  46775  fourierdlem97  46776  fourierdlem98  46777  fourierdlem99  46778  fourierdlem105  46784  fourierdlem108  46787  fourierdlem110  46789  fourierdlem112  46791  fourierdlem113  46792  fouriersw  46804  etransclem24  46831  etransclem25  46832  etransclem31  46838  etransclem35  46842  etransclem37  46844  sge0val  46939  nnfoctbdjlem  47028  nnfoctbdj  47029  ovnval  47114  ovnval2  47118  ovnval2b  47125  hsphoif  47149  hoidmvval  47150  hsphoival  47152  hoidmv1lelem1  47164  hoidmv1lelem2  47165  hoidmv1lelem3  47166  hoidmv1le  47167  ovnhoi  47176  hoidifhspval  47181  hspmbllem2  47200  ovnsubadd2  47219  blenval  49203