Theorem ifbieq12d 4515

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-un 3909  df-if 4487

This theorem is used by:  csbif  4544  csbopg  4855  tz7.44-2  8392  tz7.44-3  8393  boxcutc  8937  unxpdomlem1  9214  ttrcltr  9683  updjudhcoinlf  9925  updjudhcoinrg  9926  dfac12lem1  10134  dfac12r  10137  fin23lem12  10321  fin23lem33  10335  ttukeylem3  10501  ttukey2g  10506  xaddval  13255  seqf1olem2  14085  expval  14106  ccatfval  14617  ccatval1  14621  ccatval2  14622  ccatalpha  14638  relexpsucnnr  15069  ruclem1  16293  eucalgval2  16645  setsstruct  17242  ressval  17299  gsumvalx  18740  gsumpropd  18742  gsumpropd2lem  18743  gsumress  18746  mulgval  19143  pmtrfv  19528  xrsdsval  21572  mvrfval  22141  selvfval  22281  selvvvval  22304  marrepeval  22731  marepveval  22736  mdetunilem9  22788  madutpos  22810  madugsum  22811  minmar1eval  22817  symgmatr01lem  22821  symgmatr01  22822  gsummatr01lem3  22825  gsummatr01lem4  22826  gsummatr01  22827  ptcmplem3  24222  xrhmeo  25116  phtpycc  25161  pcovalg  25182  pcocn  25187  pcohtpylem  25189  pcoass  25194  pcorevlem  25196  ovolunlem1a  25666  ovolunlem1  25667  ioombl1  25732  mbfmax  25819  mbfpos  25821  mbfi1fseqlem2  25886  mbfi1fseq  25891  ditgeq1  26018  ditgeq2  26019  ig1pval  26344  plyn0mulidp  26453  cxpval  26840  lgamgulmlem4  27207  lgamgulmlem5  27208  musumsum  27367  muinv  27368  lgsval  27476  gausslemma2dlem1a  27540  gausslemma2dlem2  27542  gausslemma2dlem3  27543  gausslemma2dlem4  27544  abssval  28443  expsval  28629  vtxval  29361  iedgval  29362  crctcshwlkn0lem2  30171  crctcshwlkn0lem3  30172  crctcshlem4  30180  crctcsh  30184  clwlkclwwlklem2fv1  30357  eucrct2eupth  30607  ccatws1f1o  33280  psgnfzto1stlem  33429  resvval  33658  esplyfv1  33968  smatrcl  34195  smatlem  34196  madjusmdetlem2  34227  madjusmdet  34230  ballotlemsv  34909  ballotlemsf1o  34913  mrsubcv  36010  mrsubrn  36013  rdgprc0  36291  dfrdg2  36293  ditgeq123dv  36761  cbvditgdavw2  36838  csbrdgg  38003  csbfinxpg  38062  finxpreclem3  38067  poimirlem2  38301  poimirlem23  38322  poimirlem24  38323  poimirlem27  38326  itg2addnclem3  38352  itgaddnclem2  38358  ftc1anclem5  38376  cdleme27b  41170  cdleme29b  41177  cdleme31sn  41182  cdleme31fv  41192  cdleme40v  41271  dihffval  42032  dihfval  42033  dihval  42034  prjspnfv01  43384  prjspner01  43385  prjspner1  43386  aomclem8  43816  mnringvald  44965  icccncfext  46629  dvnxpaek  46684  fourierdlem103  46951  fourierdlem104  46952  ioorrnopn  47047  ioorrnopnxr  47049  hsphoival  47321  sge0hsphoire  47331  hoidmvlelem1  47337  hoidmvlelem2  47338  hoidmvlelem3  47339  hoidmvlelem4  47340  hoidmvlelem5  47341  hoidifhspval3  47361  hspmbllem2  47369  ovolval4  47393  afv2eq12d  47980