Theorem ifbieq2d 4494

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-if 4468

This theorem is referenced by:  tz7.44-2  8339  tz7.44-3  8340  oev  8442  cantnfp1lem1  9590  cantnfp1lem3  9592  ttrclselem2  9638  fin23lem12  10244  fin23lem33  10258  axcc2  10350  ttukeylem3  10424  ttukey2g  10429  canthp1lem2  10567  canthp1  10568  xnegeq  13150  xaddval  13166  xmulval  13168  expval  14016  cshfn  14743  ofccat  14922  relexpsucnnr  14978  sgnval  15041  sadcp1  16415  smupp1  16440  gcdval  16456  gcdass  16507  lcmval  16552  lcmass  16574  lcmfval  16581  lcmf0val  16582  lcmfpr  16587  iserodd  16797  pcval  16806  vdwlem6  16948  ramub1lem2  16989  ramcl  16991  mulgval  19038  symgextfv  19384  symgfixfo  19405  odfval  19498  odval  19500  submod  19535  gexval  19544  znval  21525  fvmptnn04if  22824  cpmadumatpoly  22858  cayleyhamilton  22865  cayleyhamiltonALT  22866  ptcmplem2  24028  iccpnfhmeo  24922  pcopt  24999  ioombl1  25539  ioorval  25551  uniioombllem6  25565  itg1addlem3  25675  itg2uba  25720  limcfval  25849  limcmpt  25860  limcco  25870  dvcobr  25923  ig1pval  26151  abelthlem9  26418  logtayllem  26636  logtayl  26637  leibpilem2  26918  rlimcnp2  26943  efrlim  26946  efrlimOLD  26947  igamval  27024  muval  27109  lgsval  27278  lgsfval  27279  lgsval2lem  27284  rpvmasum2  27489  padicval  27594  padicabv  27607  expsval  28431  axlowdimlem15  29039  axlowdim  29044  eupth2lem3lem3  30315  eupth2  30324  eucrct2eupth  30330  psgnfzto1stlem  33176  sgnsv  33236  sgnsval  33237  madjusmdetlem2  33988  madjusmdet  33991  xrge0iifcv  34094  xrge0iifhom  34097  xrge0tmd  34105  xrge0tmdALT  34106  signspval  34712  ex-sategoelel  35619  rdgprc0  35989  dfrdg2  35991  dfrdg4  36149  csbrdgg  37659  finxpeq1  37716  finxpreclem3  37723  poimirlem1  37956  poimirlem7  37962  poimirlem10  37965  poimirlem11  37966  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  fdc  38080  heiborlem4  38149  heiborlem6  38151  heiborlem10  38155  mapdhval  42184  hdmap1fval  42256  hdmap1vallem  42257  hdmap1val  42258  hdmap1cbv  42262  sticksstones10  42608  sticksstones12a  42610  fsuppind  43037  irrapxlem4  43271  clsk1indlem0  44486  clsk1indlem2  44487  clsk1indlem3  44488  clsk1indlem4  44489  clsk1indlem1  44490  dirkerval2  46540  dirkeritg  46548  dirkercncf  46553  fourierdlem29  46582  fourierdlem37  46590  fourierdlem62  46614  fourierdlem79  46631  fourierdlem81  46633  fourierdlem82  46634  fourierdlem92  46644  fourierdlem96  46648  fourierdlem97  46649  fourierdlem98  46650  fourierdlem99  46651  fourierdlem105  46657  fourierdlem108  46660  fourierdlem110  46662  fourierdlem112  46664  fourierdlem113  46665  fouriersw  46677  etransclem24  46704  etransclem25  46705  etransclem31  46711  etransclem35  46715  etransclem37  46717  sge0val  46812  nnfoctbdjlem  46901  nnfoctbdj  46902  ovnval  46987  ovnval2  46991  ovnval2b  46998  hsphoif  47022  hoidmvval  47023  hsphoival  47025  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1lelem3  47039  hoidmv1le  47040  ovnhoi  47049  hoidifhspval  47054  hspmbllem2  47073  ovnsubadd2  47092  blenval  49059