Theorem ifbieq12d 4485

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-un 3889  df-if 4457

This theorem is referenced by:  csbif  4514  csbopg  4824  tz7.44-2  8340  tz7.44-3  8341  boxcutc  8883  unxpdomlem1  9160  ttrcltr  9632  updjudhcoinlf  9851  updjudhcoinrg  9852  dfac12lem1  10061  dfac12r  10064  fin23lem12  10249  fin23lem33  10263  ttukeylem3  10429  ttukey2g  10434  xaddval  13170  seqf1olem2  13999  expval  14020  ccatfval  14530  ccatval1  14534  ccatval2  14535  ccatalpha  14551  relexpsucnnr  14982  ruclem1  16193  eucalgval2  16545  setsstruct  17141  ressval  17198  gsumvalx  18639  gsumpropd  18641  gsumpropd2lem  18642  gsumress  18645  mulgval  19042  pmtrfv  19421  xrsdsval  21389  mvrfval  21958  selvfval  22098  selvvvval  22121  marrepeval  22549  marepveval  22554  mdetunilem9  22606  madutpos  22628  madugsum  22629  minmar1eval  22635  symgmatr01lem  22639  symgmatr01  22640  gsummatr01lem3  22643  gsummatr01lem4  22644  gsummatr01  22645  ptcmplem3  24040  xrhmeo  24934  phtpycc  24979  pcovalg  25000  pcocn  25005  pcohtpylem  25007  pcoass  25012  pcorevlem  25014  ovolunlem1a  25484  ovolunlem1  25485  ioombl1  25550  mbfmax  25637  mbfpos  25639  mbfi1fseqlem2  25704  mbfi1fseq  25709  ditgeq1  25836  ditgeq2  25837  ig1pval  26162  cxpval  26649  lgamgulmlem4  27016  lgamgulmlem5  27017  musumsum  27176  muinv  27177  lgsval  27285  gausslemma2dlem1a  27349  gausslemma2dlem2  27351  gausslemma2dlem3  27352  gausslemma2dlem4  27353  abssval  28251  expsval  28437  vtxval  29089  iedgval  29090  crctcshwlkn0lem2  29899  crctcshwlkn0lem3  29900  crctcshlem4  29908  crctcsh  29912  clwlkclwwlklem2fv1  30085  eucrct2eupth  30335  ccatws1f1o  33032  psgnfzto1stlem  33183  resvval  33414  esplyfv1  33763  smatrcl  33990  smatlem  33991  madjusmdetlem2  34022  madjusmdet  34025  ballotlemsv  34704  ballotlemsf1o  34708  plymulx0  34741  mrsubcv  35751  mrsubrn  35754  rdgprc0  36032  dfrdg2  36034  ditgeq123dv  36462  cbvditgdavw2  36539  csbrdgg  37704  csbfinxpg  37763  finxpreclem3  37768  poimirlem2  38002  poimirlem23  38023  poimirlem24  38024  poimirlem27  38027  itg2addnclem3  38053  itgaddnclem2  38059  ftc1anclem5  38077  cdleme27b  40873  cdleme29b  40880  cdleme31sn  40885  cdleme31fv  40895  cdleme40v  40974  dihffval  41735  dihfval  41736  dihval  41737  prjspnfv01  43087  prjspner01  43088  prjspner1  43089  aomclem8  43519  mnringvald  44670  icccncfext  46342  dvnxpaek  46397  fourierdlem103  46664  fourierdlem104  46665  ioorrnopn  46760  ioorrnopnxr  46762  hsphoival  47034  sge0hsphoire  47044  hoidmvlelem1  47050  hoidmvlelem2  47051  hoidmvlelem3  47052  hoidmvlelem4  47053  hoidmvlelem5  47054  hoidifhspval3  47074  hspmbllem2  47082  ovolval4  47106  afv2eq12d  47690