Theorem ifbieq2d 4553

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-un 3952  df-if 4528

This theorem is referenced by:  tz7.44-2  8409  tz7.44-3  8410  oev  8516  cantnfp1lem1  9675  cantnfp1lem3  9677  ttrclselem2  9723  fin23lem12  10328  fin23lem33  10342  axcc2  10434  ttukeylem3  10508  ttukey2g  10513  canthp1lem2  10650  canthp1  10651  xnegeq  13190  xaddval  13206  xmulval  13208  expval  14033  cshfn  14744  ofccat  14920  relexpsucnnr  14976  sgnval  15039  sadcp1  16400  smupp1  16425  gcdval  16441  gcdass  16493  lcmval  16533  lcmass  16555  lcmfval  16562  lcmf0val  16563  lcmfpr  16568  iserodd  16772  pcval  16781  vdwlem6  16923  ramub1lem2  16964  ramcl  16966  mulgval  18990  symgextfv  19327  symgfixfo  19348  odfval  19441  odval  19443  submod  19478  gexval  19487  znval  21306  fvmptnn04if  22571  cpmadumatpoly  22605  cayleyhamilton  22612  cayleyhamiltonALT  22613  ptcmplem2  23777  iccpnfhmeo  24690  pcopt  24769  ioombl1  25311  ioorval  25323  uniioombllem6  25337  itg1addlem3  25447  itg2uba  25493  limcfval  25621  limcmpt  25632  limcco  25642  dvcobr  25697  dvcobrOLD  25698  ig1pval  25925  abelthlem9  26188  logtayllem  26403  logtayl  26404  leibpilem2  26682  rlimcnp2  26707  efrlim  26710  igamval  26787  muval  26872  lgsval  27040  lgsfval  27041  lgsval2lem  27046  rpvmasum2  27251  padicval  27356  padicabv  27369  axlowdimlem15  28481  axlowdim  28486  eupth2lem3lem3  29750  eupth2  29759  eucrct2eupth  29765  psgnfzto1stlem  32529  sgnsv  32589  sgnsval  32590  madjusmdetlem2  33106  madjusmdet  33109  xrge0iifcv  33212  xrge0iifhom  33215  xrge0tmd  33223  xrge0tmdALT  33224  signspval  33861  ex-sategoelel  34710  rdgprc0  35069  dfrdg2  35071  dfrdg4  35227  csbrdgg  36513  finxpeq1  36570  finxpreclem3  36577  poimirlem1  36792  poimirlem7  36798  poimirlem10  36801  poimirlem11  36802  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  fdc  36916  heiborlem4  36985  heiborlem6  36987  heiborlem10  36991  mapdhval  40898  hdmap1fval  40970  hdmap1vallem  40971  hdmap1val  40972  hdmap1cbv  40976  sticksstones10  41277  sticksstones12a  41279  metakunt3  41293  metakunt4  41294  metakunt6  41296  metakunt7  41297  metakunt8  41298  metakunt10  41300  metakunt11  41301  metakunt12  41302  metakunt20  41310  metakunt21  41311  metakunt22  41312  fsuppind  41464  irrapxlem4  41865  clsk1indlem0  43094  clsk1indlem2  43095  clsk1indlem3  43096  clsk1indlem4  43097  clsk1indlem1  43098  dirkerval2  45108  dirkeritg  45116  dirkercncf  45121  fourierdlem29  45150  fourierdlem37  45158  fourierdlem62  45182  fourierdlem79  45199  fourierdlem81  45201  fourierdlem82  45202  fourierdlem92  45212  fourierdlem96  45216  fourierdlem97  45217  fourierdlem98  45218  fourierdlem99  45219  fourierdlem105  45225  fourierdlem108  45228  fourierdlem110  45230  fourierdlem112  45232  fourierdlem113  45233  fouriersw  45245  etransclem24  45272  etransclem25  45273  etransclem31  45279  etransclem35  45283  etransclem37  45285  sge0val  45380  nnfoctbdjlem  45469  nnfoctbdj  45470  ovnval  45555  ovnval2  45559  ovnval2b  45566  hsphoif  45590  hoidmvval  45591  hsphoival  45593  hoidmv1lelem1  45605  hoidmv1lelem2  45606  hoidmv1lelem3  45607  hoidmv1le  45608  ovnhoi  45617  hoidifhspval  45622  hspmbllem2  45641  ovnsubadd2  45660  blenval  47344