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 2796	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568  ifcif 4486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-un 3909  df-if 4487

This theorem is referenced by:  csbif  4544  csbopg  4855  tz7.44-2  8393  tz7.44-3  8394  boxcutc  8938  unxpdomlem1  9215  ttrcltr  9684  updjudhcoinlf  9917  updjudhcoinrg  9918  dfac12lem1  10126  dfac12r  10129  fin23lem12  10314  fin23lem33  10328  ttukeylem3  10494  ttukey2g  10499  xaddval  13248  seqf1olem2  14077  expval  14098  ccatfval  14609  ccatval1  14613  ccatval2  14614  ccatalpha  14630  relexpsucnnr  15061  ruclem1  16286  eucalgval2  16638  setsstruct  17235  ressval  17292  gsumvalx  18733  gsumpropd  18735  gsumpropd2lem  18736  gsumress  18739  mulgval  19136  pmtrfv  19521  xrsdsval  21540  mvrfval  22109  selvfval  22249  selvvvval  22272  marrepeval  22699  marepveval  22704  mdetunilem9  22756  madutpos  22778  madugsum  22779  minmar1eval  22785  symgmatr01lem  22789  symgmatr01  22790  gsummatr01lem3  22793  gsummatr01lem4  22794  gsummatr01  22795  ptcmplem3  24190  xrhmeo  25084  phtpycc  25129  pcovalg  25150  pcocn  25155  pcohtpylem  25157  pcoass  25162  pcorevlem  25164  ovolunlem1a  25634  ovolunlem1  25635  ioombl1  25700  mbfmax  25787  mbfpos  25789  mbfi1fseqlem2  25854  mbfi1fseq  25859  ditgeq1  25986  ditgeq2  25987  ig1pval  26312  plyn0mulidp  26421  cxpval  26805  lgamgulmlem4  27172  lgamgulmlem5  27173  musumsum  27332  muinv  27333  lgsval  27441  gausslemma2dlem1a  27505  gausslemma2dlem2  27507  gausslemma2dlem3  27508  gausslemma2dlem4  27509  abssval  28408  expsval  28594  vtxval  29316  iedgval  29317  crctcshwlkn0lem2  30126  crctcshwlkn0lem3  30127  crctcshlem4  30135  crctcsh  30139  clwlkclwwlklem2fv1  30312  eucrct2eupth  30562  ccatws1f1o  33237  psgnfzto1stlem  33386  resvval  33615  esplyfv1  33925  smatrcl  34152  smatlem  34153  madjusmdetlem2  34184  madjusmdet  34187  ballotlemsv  34866  ballotlemsf1o  34870  mrsubcv  35956  mrsubrn  35959  rdgprc0  36237  dfrdg2  36239  ditgeq123dv  36677  cbvditgdavw2  36754  csbrdgg  37919  csbfinxpg  37978  finxpreclem3  37983  poimirlem2  38217  poimirlem23  38238  poimirlem24  38239  poimirlem27  38242  itg2addnclem3  38268  itgaddnclem2  38274  ftc1anclem5  38292  cdleme27b  41088  cdleme29b  41095  cdleme31sn  41100  cdleme31fv  41110  cdleme40v  41189  dihffval  41950  dihfval  41951  dihval  41952  prjspnfv01  43304  prjspner01  43305  prjspner1  43306  aomclem8  43736  mnringvald  44885  icccncfext  46549  dvnxpaek  46604  fourierdlem103  46871  fourierdlem104  46872  ioorrnopn  46967  ioorrnopnxr  46969  hsphoival  47241  sge0hsphoire  47251  hoidmvlelem1  47257  hoidmvlelem2  47258  hoidmvlelem3  47259  hoidmvlelem4  47260  hoidmvlelem5  47261  hoidifhspval3  47281  hspmbllem2  47289  ovolval4  47313  afv2eq12d  47897