Theorem ifbieq2d 4509

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

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-if 4483

This theorem is used by:  tz7.44-2  8396  tz7.44-3  8397  oev  8501  cantnfp1lem1  9657  cantnfp1lem3  9659  ttrclselem2  9705  fin23lem12  10333  fin23lem33  10347  axcc2  10439  ttukeylem3  10513  ttukey2g  10518  canthp1lem2  10662  canthp1  10663  xnegeq  13259  xaddval  13275  xmulval  13277  expval  14127  cshfn  14861  ofccat  15042  relexpsucnnr  15098  sgnval  15161  sadcp1  16545  smupp1  16570  gcdval  16586  gcdass  16637  lcmval  16682  lcmass  16704  lcmfval  16711  lcmf0val  16712  lcmfpr  16717  iserodd  16927  pcval  16936  vdwlem6  17078  ramub1lem2  17119  ramcl  17121  mulgval  19194  symgextfv  19545  symgfixfo  19566  odfval  19659  odval  19661  submod  19696  gexval  19705  znval  21748  fvmptnn04if  23074  cpmadumatpoly  23108  cayleyhamilton  23115  cayleyhamiltonALT  23116  ptcmplem2  24279  iccpnfhmeo  25173  pcopt  25250  ioombl1  25790  ioorval  25802  uniioombllem6  25816  itg1addlem3  25926  itg2uba  25971  limcfval  26099  limcmpt  26110  limcco  26120  dvcobr  26173  ig1pval  26401  abelthlem9  26676  logtayllem  26896  logtayl  26897  leibpilem2  27178  rlimcnp2  27203  efrlim  27206  igamval  27283  muval  27368  lgsval  27537  lgsfval  27538  lgsval2lem  27543  rpvmasum2  27748  padicval  27853  padicabv  27866  expsval  28690  axlowdimlem15  29413  axlowdim  29418  eupth2lem3lem3  30710  eupth2  30719  eucrct2eupth  30725  psgnfzto1stlem  33540  sgnsv  33600  sgnsval  33601  madjusmdetlem2  34338  madjusmdet  34341  xrge0iifcv  34444  xrge0iifhom  34447  xrge0tmd  34455  xrge0tmdALT  34456  signspval  35060  ex-sategoelel  36000  rdgprc0  36370  dfrdg2  36372  dfrdg4  36530  csbrdgg  38083  finxpeq1  38140  finxpreclem3  38147  poimirlem1  38370  poimirlem7  38376  poimirlem10  38379  poimirlem11  38380  itg2addnclem  38420  itg2addnclem3  38422  itg2addnc  38423  fdc  38495  heiborlem4  38564  heiborlem6  38566  heiborlem10  38570  mapdhval  42597  hdmap1fval  42669  hdmap1vallem  42670  hdmap1val  42671  hdmap1cbv  42675  sticksstones10  43021  sticksstones12a  43023  fsuppind  43436  irrapxlem4  43666  clsk1indlem0  44881  clsk1indlem2  44882  clsk1indlem3  44883  clsk1indlem4  44884  clsk1indlem1  44885  dirkerval2  46922  dirkeritg  46930  dirkercncf  46935  fourierdlem29  46964  fourierdlem37  46972  fourierdlem62  46996  fourierdlem79  47013  fourierdlem81  47015  fourierdlem82  47016  fourierdlem92  47026  fourierdlem96  47030  fourierdlem97  47031  fourierdlem98  47032  fourierdlem99  47033  fourierdlem105  47039  fourierdlem108  47042  fourierdlem110  47044  fourierdlem112  47046  fourierdlem113  47047  fouriersw  47059  etransclem24  47086  etransclem25  47087  etransclem31  47093  etransclem35  47097  etransclem37  47099  sge0val  47194  nnfoctbdjlem  47283  nnfoctbdj  47284  ovnval  47369  ovnval2  47373  ovnval2b  47380  hsphoif  47404  hoidmvval  47405  hsphoival  47407  hoidmv1lelem1  47419  hoidmv1lelem2  47420  hoidmv1lelem3  47421  hoidmv1le  47422  ovnhoi  47431  hoidifhspval  47436  hspmbllem2  47455  ovnsubadd2  47474  blenval  49501