Theorem ifbieq12d 4576

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-if 4549

This theorem is referenced by:  csbif  4605  csbopg  4915  tz7.44-2  8463  tz7.44-3  8464  boxcutc  8999  unxpdomlem1  9313  ttrcltr  9785  updjudhcoinlf  10001  updjudhcoinrg  10002  dfac12lem1  10213  dfac12r  10216  fin23lem12  10400  fin23lem33  10414  ttukeylem3  10580  ttukey2g  10585  xaddval  13285  seqf1olem2  14093  expval  14114  ccatfval  14621  ccatval1  14625  ccatval2  14626  ccatalpha  14641  relexpsucnnr  15074  ruclem1  16279  eucalgval2  16628  setsstruct  17223  ressval  17290  gsumvalx  18714  gsumpropd  18716  gsumpropd2lem  18717  gsumress  18720  mulgval  19111  pmtrfv  19494  xrsdsval  21451  mvrfval  22024  selvfval  22161  marrepeval  22590  marepveval  22595  mdetunilem9  22647  madutpos  22669  madugsum  22670  minmar1eval  22676  symgmatr01lem  22680  symgmatr01  22681  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  ptcmplem3  24083  xrhmeo  24996  phtpycc  25042  pcovalg  25064  pcocn  25069  pcohtpylem  25071  pcoass  25076  pcorevlem  25078  ovolunlem1a  25550  ovolunlem1  25551  ioombl1  25616  mbfmax  25703  mbfpos  25705  mbfi1fseqlem2  25771  mbfi1fseq  25776  ditgeq1  25903  ditgeq2  25904  ig1pval  26235  cxpval  26724  lgamgulmlem4  27093  lgamgulmlem5  27094  musumsum  27253  muinv  27254  lgsval  27363  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  gausslemma2dlem3  27430  gausslemma2dlem4  27431  abssval  28281  expsval  28426  vtxval  29035  iedgval  29036  crctcshwlkn0lem2  29844  crctcshwlkn0lem3  29845  crctcshlem4  29853  crctcsh  29857  clwlkclwwlklem2fv1  30027  eucrct2eupth  30277  ccatws1f1o  32918  psgnfzto1stlem  33093  resvval  33318  smatrcl  33742  smatlem  33743  madjusmdetlem2  33774  madjusmdet  33777  ballotlemsv  34474  ballotlemsf1o  34478  plymulx0  34524  mrsubcv  35478  mrsubrn  35481  rdgprc0  35757  dfrdg2  35759  ditgeq123dv  36187  cbvditgdavw2  36264  csbrdgg  37295  csbfinxpg  37354  finxpreclem3  37359  poimirlem2  37582  poimirlem23  37603  poimirlem24  37604  poimirlem27  37607  itg2addnclem3  37633  itgaddnclem2  37639  ftc1anclem5  37657  cdleme27b  40325  cdleme29b  40332  cdleme31sn  40337  cdleme31fv  40347  cdleme40v  40426  dihffval  41187  dihfval  41188  dihval  41189  metakunt3  42164  metakunt4  42165  metakunt6  42167  metakunt7  42168  metakunt8  42169  metakunt10  42171  metakunt11  42172  metakunt12  42173  metakunt20  42181  metakunt21  42182  metakunt22  42183  metakunt32  42193  selvvvval  42540  prjspnfv01  42579  prjspner01  42580  prjspner1  42581  aomclem8  43018  mnringvald  44177  icccncfext  45808  dvnxpaek  45863  fourierdlem103  46130  fourierdlem104  46131  ioorrnopn  46226  ioorrnopnxr  46228  hsphoival  46500  sge0hsphoire  46510  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvlelem5  46520  hoidifhspval3  46540  hspmbllem2  46548  ovolval4  46572  afv2eq12d  47130