Theorem ifbieq12d 4529

Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
ifbieq12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq12d.2	⊢ (𝜑 → 𝐴 = 𝐶)
ifbieq12d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
ifbieq12d	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))

Proof of Theorem ifbieq12d

Step	Hyp	Ref	Expression
1		ifbieq12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 4524	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3		ifbieq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4		ifbieq12d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	ifeq12d 4522	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
6	2, 5	eqtrd 2770	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-un 3931  df-if 4501

This theorem is referenced by:  csbif  4558  csbopg  4867  tz7.44-2  8421  tz7.44-3  8422  boxcutc  8955  unxpdomlem1  9258  ttrcltr  9730  updjudhcoinlf  9946  updjudhcoinrg  9947  dfac12lem1  10158  dfac12r  10161  fin23lem12  10345  fin23lem33  10359  ttukeylem3  10525  ttukey2g  10530  xaddval  13239  seqf1olem2  14060  expval  14081  ccatfval  14591  ccatval1  14595  ccatval2  14596  ccatalpha  14611  relexpsucnnr  15044  ruclem1  16249  eucalgval2  16600  setsstruct  17195  ressval  17254  gsumvalx  18654  gsumpropd  18656  gsumpropd2lem  18657  gsumress  18660  mulgval  19054  pmtrfv  19433  xrsdsval  21378  mvrfval  21941  selvfval  22072  marrepeval  22501  marepveval  22506  mdetunilem9  22558  madutpos  22580  madugsum  22581  minmar1eval  22587  symgmatr01lem  22591  symgmatr01  22592  gsummatr01lem3  22595  gsummatr01lem4  22596  gsummatr01  22597  ptcmplem3  23992  xrhmeo  24895  phtpycc  24941  pcovalg  24963  pcocn  24968  pcohtpylem  24970  pcoass  24975  pcorevlem  24977  ovolunlem1a  25449  ovolunlem1  25450  ioombl1  25515  mbfmax  25602  mbfpos  25604  mbfi1fseqlem2  25669  mbfi1fseq  25674  ditgeq1  25801  ditgeq2  25802  ig1pval  26133  cxpval  26625  lgamgulmlem4  26994  lgamgulmlem5  26995  musumsum  27154  muinv  27155  lgsval  27264  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem3  27331  gausslemma2dlem4  27332  abssval  28193  expsval  28363  vtxval  28979  iedgval  28980  crctcshwlkn0lem2  29793  crctcshwlkn0lem3  29794  crctcshlem4  29802  crctcsh  29806  clwlkclwwlklem2fv1  29976  eucrct2eupth  30226  ccatws1f1o  32927  psgnfzto1stlem  33111  resvval  33345  smatrcl  33827  smatlem  33828  madjusmdetlem2  33859  madjusmdet  33862  ballotlemsv  34542  ballotlemsf1o  34546  plymulx0  34579  mrsubcv  35532  mrsubrn  35535  rdgprc0  35811  dfrdg2  35813  ditgeq123dv  36239  cbvditgdavw2  36316  csbrdgg  37347  csbfinxpg  37406  finxpreclem3  37411  poimirlem2  37646  poimirlem23  37667  poimirlem24  37668  poimirlem27  37671  itg2addnclem3  37697  itgaddnclem2  37703  ftc1anclem5  37721  cdleme27b  40387  cdleme29b  40394  cdleme31sn  40399  cdleme31fv  40409  cdleme40v  40488  dihffval  41249  dihfval  41250  dihval  41251  metakunt3  42220  metakunt4  42221  metakunt6  42223  metakunt7  42224  metakunt8  42225  metakunt10  42227  metakunt11  42228  metakunt12  42229  metakunt20  42237  metakunt21  42238  metakunt22  42239  metakunt32  42249  selvvvval  42608  prjspnfv01  42647  prjspner01  42648  prjspner1  42649  aomclem8  43085  mnringvald  44237  icccncfext  45916  dvnxpaek  45971  fourierdlem103  46238  fourierdlem104  46239  ioorrnopn  46334  ioorrnopnxr  46336  hsphoival  46608  sge0hsphoire  46618  hoidmvlelem1  46624  hoidmvlelem2  46625  hoidmvlelem3  46626  hoidmvlelem4  46627  hoidmvlelem5  46628  hoidifhspval3  46648  hspmbllem2  46656  ovolval4  46680  afv2eq12d  47244