Theorem ifbieq2d 4512

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-un 4154  df-if 4486

This theorem is used by:  tz7.44-2  8451  tz7.44-3  8452  oev  8558  cantnfp1lem1  9714  cantnfp1lem3  9716  ttrclselem2  9762  fin23lem12  10446  fin23lem33  10460  axcc2  10552  ttukeylem3  10626  ttukey2g  10631  canthp1lem2  10775  canthp1  10776  xnegeq  13375  xaddval  13391  xmulval  13393  expval  14244  cshfn  14981  ofccat  15163  relexpsucnnr  15219  sgnval  15282  sadcp1  16666  smupp1  16691  gcdval  16707  gcdass  16761  lcmval  16808  lcmass  16830  lcmfval  16837  lcmf0val  16838  lcmfpr  16843  iserodd  17054  pcval  17063  vdwlem6  17205  ramub1lem2  17246  ramcl  17248  mulgval  19322  symgextfv  19674  symgfixfo  19695  odfval  19788  odval  19790  submod  19825  gexval  19834  znval  21885  fvmptnn04if  23211  cpmadumatpoly  23245  cayleyhamilton  23252  cayleyhamiltonALT  23253  ptcmplem2  24416  iccpnfhmeo  25310  pcopt  25387  ioombl1  25927  ioorval  25939  uniioombllem6  25953  itg1addlem3  26063  itg2uba  26108  limcfval  26236  limcmpt  26247  limcco  26257  dvcobr  26310  ig1pval  26538  abelthlem9  26813  logtayllem  27033  logtayl  27034  leibpilem2  27315  rlimcnp2  27340  efrlim  27343  igamval  27420  muval  27505  lgsval  27674  lgsfval  27675  lgsval2lem  27680  rpvmasum2  27885  padicval  27990  padicabv  28003  expsval  28857  axlowdimlem15  29580  axlowdim  29585  eupth2lem3lem3  30877  eupth2  30886  eucrct2eupth  30892  psgnfzto1stlem  33750  sgnsv  33810  sgnsval  33811  madjusmdetlem2  34564  madjusmdet  34567  xrge0iifcv  34670  xrge0iifhom  34673  xrge0tmd  34681  xrge0tmdALT  34682  signspval  35285  ex-sategoelel  36387  rdgprc0  36763  dfrdg2  36765  dfrdg4  36923  csbrdgg  38513  finxpeq1  38570  finxpreclem3  38577  poimirlem1  38800  poimirlem7  38806  poimirlem10  38809  poimirlem11  38810  itg2addnclem  38850  itg2addnclem3  38852  itg2addnc  38853  fdc  38938  heiborlem4  39007  heiborlem6  39009  heiborlem10  39013  mapdhval  43040  hdmap1fval  43112  hdmap1vallem  43113  hdmap1val  43114  hdmap1cbv  43118  sticksstones10  43464  sticksstones12a  43466  fsuppind  43878  irrapxlem4  44092  clsk1indlem0  45296  clsk1indlem2  45297  clsk1indlem3  45298  clsk1indlem4  45299  clsk1indlem1  45300  dirkerval2  47371  dirkeritg  47379  dirkercncf  47384  fourierdlem29  47413  fourierdlem37  47421  fourierdlem62  47445  fourierdlem79  47462  fourierdlem81  47464  fourierdlem82  47465  fourierdlem92  47475  fourierdlem96  47479  fourierdlem97  47480  fourierdlem98  47481  fourierdlem99  47482  fourierdlem105  47488  fourierdlem108  47491  fourierdlem110  47493  fourierdlem112  47495  fourierdlem113  47496  fouriersw  47508  etransclem24  47535  etransclem25  47536  etransclem31  47542  etransclem35  47546  etransclem37  47548  sge0val  47643  nnfoctbdjlem  47732  nnfoctbdj  47733  ovnval  47818  ovnval2  47822  ovnval2b  47829  hsphoif  47853  hoidmvval  47854  hsphoival  47856  hoidmv1lelem1  47868  hoidmv1lelem2  47869  hoidmv1lelem3  47870  hoidmv1le  47871  ovnhoi  47880  hoidifhspval  47885  hspmbllem2  47904  ovnsubadd2  47923  blenval  50008  parhomval  51068  parhomvaln0  51078  parswapval  51101