Theorem ifbieq12d 4508

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 4503	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3		ifbieq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4		ifbieq12d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	ifeq12d 4501	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
6	2, 5	eqtrd 2771	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-if 4480

This theorem is referenced by:  csbif  4537  csbopg  4847  tz7.44-2  8338  tz7.44-3  8339  boxcutc  8879  unxpdomlem1  9156  ttrcltr  9625  updjudhcoinlf  9844  updjudhcoinrg  9845  dfac12lem1  10054  dfac12r  10057  fin23lem12  10241  fin23lem33  10255  ttukeylem3  10421  ttukey2g  10426  xaddval  13138  seqf1olem2  13965  expval  13986  ccatfval  14496  ccatval1  14500  ccatval2  14501  ccatalpha  14517  relexpsucnnr  14948  ruclem1  16156  eucalgval2  16508  setsstruct  17103  ressval  17160  gsumvalx  18601  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  mulgval  19001  pmtrfv  19381  xrsdsval  21365  mvrfval  21936  selvfval  22077  marrepeval  22507  marepveval  22512  mdetunilem9  22564  madutpos  22586  madugsum  22587  minmar1eval  22593  symgmatr01lem  22597  symgmatr01  22598  gsummatr01lem3  22601  gsummatr01lem4  22602  gsummatr01  22603  ptcmplem3  23998  xrhmeo  24900  phtpycc  24946  pcovalg  24968  pcocn  24973  pcohtpylem  24975  pcoass  24980  pcorevlem  24982  ovolunlem1a  25453  ovolunlem1  25454  ioombl1  25519  mbfmax  25606  mbfpos  25608  mbfi1fseqlem2  25673  mbfi1fseq  25678  ditgeq1  25805  ditgeq2  25806  ig1pval  26137  cxpval  26629  lgamgulmlem4  26998  lgamgulmlem5  26999  musumsum  27158  muinv  27159  lgsval  27268  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  gausslemma2dlem3  27335  gausslemma2dlem4  27336  abssval  28235  expsval  28421  vtxval  29073  iedgval  29074  crctcshwlkn0lem2  29884  crctcshwlkn0lem3  29885  crctcshlem4  29893  crctcsh  29897  clwlkclwwlklem2fv1  30070  eucrct2eupth  30320  ccatws1f1o  33033  psgnfzto1stlem  33182  resvval  33410  esplyfv1  33727  smatrcl  33953  smatlem  33954  madjusmdetlem2  33985  madjusmdet  33988  ballotlemsv  34667  ballotlemsf1o  34671  plymulx0  34704  mrsubcv  35704  mrsubrn  35707  rdgprc0  35985  dfrdg2  35987  ditgeq123dv  36415  cbvditgdavw2  36492  csbrdgg  37530  csbfinxpg  37589  finxpreclem3  37594  poimirlem2  37819  poimirlem23  37840  poimirlem24  37841  poimirlem27  37844  itg2addnclem3  37870  itgaddnclem2  37876  ftc1anclem5  37894  cdleme27b  40624  cdleme29b  40631  cdleme31sn  40636  cdleme31fv  40646  cdleme40v  40725  dihffval  41486  dihfval  41487  dihval  41488  selvvvval  42824  prjspnfv01  42863  prjspner01  42864  prjspner1  42865  aomclem8  43299  mnringvald  44450  icccncfext  46127  dvnxpaek  46182  fourierdlem103  46449  fourierdlem104  46450  ioorrnopn  46545  ioorrnopnxr  46547  hsphoival  46819  sge0hsphoire  46829  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem4  46838  hoidmvlelem5  46839  hoidifhspval3  46859  hspmbllem2  46867  ovolval4  46891  afv2eq12d  47457