Theorem ifbieq2d 4552

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-if 4526

This theorem is referenced by:  tz7.44-2  8447  tz7.44-3  8448  oev  8552  cantnfp1lem1  9718  cantnfp1lem3  9720  ttrclselem2  9766  fin23lem12  10371  fin23lem33  10385  axcc2  10477  ttukeylem3  10551  ttukey2g  10556  canthp1lem2  10693  canthp1  10694  xnegeq  13249  xaddval  13265  xmulval  13267  expval  14104  cshfn  14828  ofccat  15008  relexpsucnnr  15064  sgnval  15127  sadcp1  16492  smupp1  16517  gcdval  16533  gcdass  16584  lcmval  16629  lcmass  16651  lcmfval  16658  lcmf0val  16659  lcmfpr  16664  iserodd  16873  pcval  16882  vdwlem6  17024  ramub1lem2  17065  ramcl  17067  mulgval  19089  symgextfv  19436  symgfixfo  19457  odfval  19550  odval  19552  submod  19587  gexval  19596  znval  21550  fvmptnn04if  22855  cpmadumatpoly  22889  cayleyhamilton  22896  cayleyhamiltonALT  22897  ptcmplem2  24061  iccpnfhmeo  24976  pcopt  25055  ioombl1  25597  ioorval  25609  uniioombllem6  25623  itg1addlem3  25733  itg2uba  25778  limcfval  25907  limcmpt  25918  limcco  25928  dvcobr  25983  dvcobrOLD  25984  ig1pval  26215  abelthlem9  26484  logtayllem  26701  logtayl  26702  leibpilem2  26984  rlimcnp2  27009  efrlim  27012  efrlimOLD  27013  igamval  27090  muval  27175  lgsval  27345  lgsfval  27346  lgsval2lem  27351  rpvmasum2  27556  padicval  27661  padicabv  27674  expsval  28408  axlowdimlem15  28971  axlowdim  28976  eupth2lem3lem3  30249  eupth2  30258  eucrct2eupth  30264  psgnfzto1stlem  33120  sgnsv  33180  sgnsval  33181  madjusmdetlem2  33827  madjusmdet  33830  xrge0iifcv  33933  xrge0iifhom  33936  xrge0tmd  33944  xrge0tmdALT  33945  signspval  34567  ex-sategoelel  35426  rdgprc0  35794  dfrdg2  35796  dfrdg4  35952  csbrdgg  37330  finxpeq1  37387  finxpreclem3  37394  poimirlem1  37628  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  fdc  37752  heiborlem4  37821  heiborlem6  37823  heiborlem10  37827  mapdhval  41726  hdmap1fval  41798  hdmap1vallem  41799  hdmap1val  41800  hdmap1cbv  41804  sticksstones10  42156  sticksstones12a  42158  metakunt3  42208  metakunt4  42209  metakunt6  42211  metakunt7  42212  metakunt8  42213  metakunt10  42215  metakunt11  42216  metakunt12  42217  metakunt20  42225  metakunt21  42226  metakunt22  42227  fsuppind  42600  irrapxlem4  42836  clsk1indlem0  44054  clsk1indlem2  44055  clsk1indlem3  44056  clsk1indlem4  44057  clsk1indlem1  44058  dirkerval2  46109  dirkeritg  46117  dirkercncf  46122  fourierdlem29  46151  fourierdlem37  46159  fourierdlem62  46183  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem92  46213  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem105  46226  fourierdlem108  46229  fourierdlem110  46231  fourierdlem112  46233  fourierdlem113  46234  fouriersw  46246  etransclem24  46273  etransclem25  46274  etransclem31  46280  etransclem35  46284  etransclem37  46286  sge0val  46381  nnfoctbdjlem  46470  nnfoctbdj  46471  ovnval  46556  ovnval2  46560  ovnval2b  46567  hsphoif  46591  hoidmvval  46592  hsphoival  46594  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmv1le  46609  ovnhoi  46618  hoidifhspval  46623  hspmbllem2  46642  ovnsubadd2  46661  blenval  48492