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 2796	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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-if 4483

This theorem is used by:  tz7.44-2  8415  tz7.44-3  8416  oev  8522  cantnfp1lem1  9679  cantnfp1lem3  9681  ttrclselem2  9727  fin23lem12  10409  fin23lem33  10423  axcc2  10515  ttukeylem3  10589  ttukey2g  10594  canthp1lem2  10738  canthp1  10739  xnegeq  13337  xaddval  13353  xmulval  13355  expval  14206  cshfn  14941  ofccat  15122  relexpsucnnr  15178  sgnval  15241  sadcp1  16625  smupp1  16650  gcdval  16666  gcdass  16720  lcmval  16767  lcmass  16789  lcmfval  16796  lcmf0val  16797  lcmfpr  16802  iserodd  17013  pcval  17022  vdwlem6  17164  ramub1lem2  17205  ramcl  17207  mulgval  19281  symgextfv  19632  symgfixfo  19653  odfval  19746  odval  19748  submod  19783  gexval  19792  znval  21841  fvmptnn04if  23167  cpmadumatpoly  23201  cayleyhamilton  23208  cayleyhamiltonALT  23209  ptcmplem2  24372  iccpnfhmeo  25266  pcopt  25343  ioombl1  25883  ioorval  25895  uniioombllem6  25909  itg1addlem3  26019  itg2uba  26064  limcfval  26192  limcmpt  26203  limcco  26213  dvcobr  26266  ig1pval  26494  abelthlem9  26767  logtayllem  26987  logtayl  26988  leibpilem2  27269  rlimcnp2  27294  efrlim  27297  igamval  27374  muval  27459  lgsval  27628  lgsfval  27629  lgsval2lem  27634  rpvmasum2  27839  padicval  27944  padicabv  27957  expsval  28811  axlowdimlem15  29534  axlowdim  29539  eupth2lem3lem3  30831  eupth2  30840  eucrct2eupth  30846  psgnfzto1stlem  33661  sgnsv  33721  sgnsval  33722  madjusmdetlem2  34460  madjusmdet  34463  xrge0iifcv  34566  xrge0iifhom  34569  xrge0tmd  34577  xrge0tmdALT  34578  signspval  35181  ex-sategoelel  36186  rdgprc0  36555  dfrdg2  36557  dfrdg4  36715  csbrdgg  38252  finxpeq1  38309  finxpreclem3  38316  poimirlem1  38539  poimirlem7  38545  poimirlem10  38548  poimirlem11  38549  itg2addnclem  38589  itg2addnclem3  38591  itg2addnc  38592  fdc  38679  heiborlem4  38748  heiborlem6  38750  heiborlem10  38754  mapdhval  42781  hdmap1fval  42853  hdmap1vallem  42854  hdmap1val  42855  hdmap1cbv  42859  sticksstones10  43205  sticksstones12a  43207  fsuppind  43618  irrapxlem4  43831  clsk1indlem0  45040  clsk1indlem2  45041  clsk1indlem3  45042  clsk1indlem4  45043  clsk1indlem1  45044  dirkerval2  47103  dirkeritg  47111  dirkercncf  47116  fourierdlem29  47145  fourierdlem37  47153  fourierdlem62  47177  fourierdlem79  47194  fourierdlem81  47196  fourierdlem82  47197  fourierdlem92  47207  fourierdlem96  47211  fourierdlem97  47212  fourierdlem98  47213  fourierdlem99  47214  fourierdlem105  47220  fourierdlem108  47223  fourierdlem110  47225  fourierdlem112  47227  fourierdlem113  47228  fouriersw  47240  etransclem24  47267  etransclem25  47268  etransclem31  47274  etransclem35  47278  etransclem37  47280  sge0val  47375  nnfoctbdjlem  47464  nnfoctbdj  47465  ovnval  47550  ovnval2  47554  ovnval2b  47561  hsphoif  47585  hoidmvval  47586  hsphoival  47588  hoidmv1lelem1  47600  hoidmv1lelem2  47601  hoidmv1lelem3  47602  hoidmv1le  47603  ovnhoi  47612  hoidifhspval  47617  hspmbllem2  47636  ovnsubadd2  47655  blenval  49682