Theorem ifbieq12d 4495

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-if 4467

This theorem is referenced by:  csbif  4524  csbopg  4834  tz7.44-2  8346  tz7.44-3  8347  boxcutc  8889  unxpdomlem1  9166  ttrcltr  9637  updjudhcoinlf  9856  updjudhcoinrg  9857  dfac12lem1  10066  dfac12r  10069  fin23lem12  10253  fin23lem33  10267  ttukeylem3  10433  ttukey2g  10438  xaddval  13175  seqf1olem2  14004  expval  14025  ccatfval  14535  ccatval1  14539  ccatval2  14540  ccatalpha  14556  relexpsucnnr  14987  ruclem1  16198  eucalgval2  16550  setsstruct  17146  ressval  17203  gsumvalx  18644  gsumpropd  18646  gsumpropd2lem  18647  gsumress  18650  mulgval  19047  pmtrfv  19427  xrsdsval  21391  mvrfval  21959  selvfval  22100  marrepeval  22528  marepveval  22533  mdetunilem9  22585  madutpos  22607  madugsum  22608  minmar1eval  22614  symgmatr01lem  22618  symgmatr01  22619  gsummatr01lem3  22622  gsummatr01lem4  22623  gsummatr01  22624  ptcmplem3  24019  xrhmeo  24913  phtpycc  24958  pcovalg  24979  pcocn  24984  pcohtpylem  24986  pcoass  24991  pcorevlem  24993  ovolunlem1a  25463  ovolunlem1  25464  ioombl1  25529  mbfmax  25616  mbfpos  25618  mbfi1fseqlem2  25683  mbfi1fseq  25688  ditgeq1  25815  ditgeq2  25816  ig1pval  26141  cxpval  26628  lgamgulmlem4  26995  lgamgulmlem5  26996  musumsum  27155  muinv  27156  lgsval  27264  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem3  27331  gausslemma2dlem4  27332  abssval  28231  expsval  28417  vtxval  29069  iedgval  29070  crctcshwlkn0lem2  29879  crctcshwlkn0lem3  29880  crctcshlem4  29888  crctcsh  29892  clwlkclwwlklem2fv1  30065  eucrct2eupth  30315  ccatws1f1o  33011  psgnfzto1stlem  33161  resvval  33389  esplyfv1  33713  smatrcl  33940  smatlem  33941  madjusmdetlem2  33972  madjusmdet  33975  ballotlemsv  34654  ballotlemsf1o  34658  plymulx0  34691  mrsubcv  35692  mrsubrn  35695  rdgprc0  35973  dfrdg2  35975  ditgeq123dv  36403  cbvditgdavw2  36480  csbrdgg  37645  csbfinxpg  37704  finxpreclem3  37709  poimirlem2  37943  poimirlem23  37964  poimirlem24  37965  poimirlem27  37968  itg2addnclem3  37994  itgaddnclem2  38000  ftc1anclem5  38018  cdleme27b  40814  cdleme29b  40821  cdleme31sn  40826  cdleme31fv  40836  cdleme40v  40915  dihffval  41676  dihfval  41677  dihval  41678  selvvvval  43018  prjspnfv01  43057  prjspner01  43058  prjspner1  43059  aomclem8  43489  mnringvald  44640  icccncfext  46315  dvnxpaek  46370  fourierdlem103  46637  fourierdlem104  46638  ioorrnopn  46733  ioorrnopnxr  46735  hsphoival  47007  sge0hsphoire  47017  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hoidifhspval3  47047  hspmbllem2  47055  ovolval4  47079  afv2eq12d  47663