Theorem ifbieq2d 4503

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4476

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-un 3908  df-if 4477

This theorem is referenced by:  tz7.44-2  8329  tz7.44-3  8330  oev  8432  cantnfp1lem1  9574  cantnfp1lem3  9576  ttrclselem2  9622  fin23lem12  10225  fin23lem33  10239  axcc2  10331  ttukeylem3  10405  ttukey2g  10410  canthp1lem2  10547  canthp1  10548  xnegeq  13109  xaddval  13125  xmulval  13127  expval  13970  cshfn  14696  ofccat  14876  relexpsucnnr  14932  sgnval  14995  sadcp1  16366  smupp1  16391  gcdval  16407  gcdass  16458  lcmval  16503  lcmass  16525  lcmfval  16532  lcmf0val  16533  lcmfpr  16538  iserodd  16747  pcval  16756  vdwlem6  16898  ramub1lem2  16939  ramcl  16941  mulgval  18950  symgextfv  19297  symgfixfo  19318  odfval  19411  odval  19413  submod  19448  gexval  19457  znval  21442  fvmptnn04if  22734  cpmadumatpoly  22768  cayleyhamilton  22775  cayleyhamiltonALT  22776  ptcmplem2  23938  iccpnfhmeo  24841  pcopt  24920  ioombl1  25461  ioorval  25473  uniioombllem6  25487  itg1addlem3  25597  itg2uba  25642  limcfval  25771  limcmpt  25782  limcco  25792  dvcobr  25847  dvcobrOLD  25848  ig1pval  26079  abelthlem9  26348  logtayllem  26566  logtayl  26567  leibpilem2  26849  rlimcnp2  26874  efrlim  26877  efrlimOLD  26878  igamval  26955  muval  27040  lgsval  27210  lgsfval  27211  lgsval2lem  27216  rpvmasum2  27421  padicval  27526  padicabv  27539  expsval  28317  axlowdimlem15  28901  axlowdim  28906  eupth2lem3lem3  30174  eupth2  30183  eucrct2eupth  30189  psgnfzto1stlem  33042  sgnsv  33102  sgnsval  33103  madjusmdetlem2  33795  madjusmdet  33798  xrge0iifcv  33901  xrge0iifhom  33904  xrge0tmd  33912  xrge0tmdALT  33913  signspval  34520  ex-sategoelel  35394  rdgprc0  35767  dfrdg2  35769  dfrdg4  35925  csbrdgg  37303  finxpeq1  37360  finxpreclem3  37367  poimirlem1  37601  poimirlem7  37607  poimirlem10  37610  poimirlem11  37611  itg2addnclem  37651  itg2addnclem3  37653  itg2addnc  37654  fdc  37725  heiborlem4  37794  heiborlem6  37796  heiborlem10  37800  mapdhval  41703  hdmap1fval  41775  hdmap1vallem  41776  hdmap1val  41777  hdmap1cbv  41781  sticksstones10  42128  sticksstones12a  42130  fsuppind  42563  irrapxlem4  42798  clsk1indlem0  44014  clsk1indlem2  44015  clsk1indlem3  44016  clsk1indlem4  44017  clsk1indlem1  44018  dirkerval2  46075  dirkeritg  46083  dirkercncf  46088  fourierdlem29  46117  fourierdlem37  46125  fourierdlem62  46149  fourierdlem79  46166  fourierdlem81  46168  fourierdlem82  46169  fourierdlem92  46179  fourierdlem96  46183  fourierdlem97  46184  fourierdlem98  46185  fourierdlem99  46186  fourierdlem105  46192  fourierdlem108  46195  fourierdlem110  46197  fourierdlem112  46199  fourierdlem113  46200  fouriersw  46212  etransclem24  46239  etransclem25  46240  etransclem31  46246  etransclem35  46250  etransclem37  46252  sge0val  46347  nnfoctbdjlem  46436  nnfoctbdj  46437  ovnval  46522  ovnval2  46526  ovnval2b  46533  hsphoif  46557  hoidmvval  46558  hsphoival  46560  hoidmv1lelem1  46572  hoidmv1lelem2  46573  hoidmv1lelem3  46574  hoidmv1le  46575  ovnhoi  46584  hoidifhspval  46589  hspmbllem2  46608  ovnsubadd2  46627  blenval  48556