Theorem ifbieq12d 4507

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-un 3910  df-if 4479

This theorem is referenced by:  csbif  4536  csbopg  4845  tz7.44-2  8336  tz7.44-3  8337  boxcutc  8875  unxpdomlem1  9155  ttrcltr  9631  updjudhcoinlf  9847  updjudhcoinrg  9848  dfac12lem1  10057  dfac12r  10060  fin23lem12  10244  fin23lem33  10258  ttukeylem3  10424  ttukey2g  10429  xaddval  13143  seqf1olem2  13967  expval  13988  ccatfval  14498  ccatval1  14502  ccatval2  14503  ccatalpha  14518  relexpsucnnr  14950  ruclem1  16158  eucalgval2  16510  setsstruct  17105  ressval  17162  gsumvalx  18568  gsumpropd  18570  gsumpropd2lem  18571  gsumress  18574  mulgval  18968  pmtrfv  19349  xrsdsval  21335  mvrfval  21906  selvfval  22037  marrepeval  22466  marepveval  22471  mdetunilem9  22523  madutpos  22545  madugsum  22546  minmar1eval  22552  symgmatr01lem  22556  symgmatr01  22557  gsummatr01lem3  22560  gsummatr01lem4  22561  gsummatr01  22562  ptcmplem3  23957  xrhmeo  24860  phtpycc  24906  pcovalg  24928  pcocn  24933  pcohtpylem  24935  pcoass  24940  pcorevlem  24942  ovolunlem1a  25413  ovolunlem1  25414  ioombl1  25479  mbfmax  25566  mbfpos  25568  mbfi1fseqlem2  25633  mbfi1fseq  25638  ditgeq1  25765  ditgeq2  25766  ig1pval  26097  cxpval  26589  lgamgulmlem4  26958  lgamgulmlem5  26959  musumsum  27118  muinv  27119  lgsval  27228  gausslemma2dlem1a  27292  gausslemma2dlem2  27294  gausslemma2dlem3  27295  gausslemma2dlem4  27296  abssval  28164  expsval  28335  vtxval  28963  iedgval  28964  crctcshwlkn0lem2  29774  crctcshwlkn0lem3  29775  crctcshlem4  29783  crctcsh  29787  clwlkclwwlklem2fv1  29957  eucrct2eupth  30207  ccatws1f1o  32906  psgnfzto1stlem  33055  resvval  33277  smatrcl  33762  smatlem  33763  madjusmdetlem2  33794  madjusmdet  33797  ballotlemsv  34477  ballotlemsf1o  34481  plymulx0  34514  mrsubcv  35482  mrsubrn  35485  rdgprc0  35766  dfrdg2  35768  ditgeq123dv  36194  cbvditgdavw2  36271  csbrdgg  37302  csbfinxpg  37361  finxpreclem3  37366  poimirlem2  37601  poimirlem23  37622  poimirlem24  37623  poimirlem27  37626  itg2addnclem3  37652  itgaddnclem2  37658  ftc1anclem5  37676  cdleme27b  40347  cdleme29b  40354  cdleme31sn  40359  cdleme31fv  40369  cdleme40v  40448  dihffval  41209  dihfval  41210  dihval  41211  selvvvval  42558  prjspnfv01  42597  prjspner01  42598  prjspner1  42599  aomclem8  43034  mnringvald  44186  icccncfext  45869  dvnxpaek  45924  fourierdlem103  46191  fourierdlem104  46192  ioorrnopn  46287  ioorrnopnxr  46289  hsphoival  46561  sge0hsphoire  46571  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem4  46580  hoidmvlelem5  46581  hoidifhspval3  46601  hspmbllem2  46609  ovolval4  46633  afv2eq12d  47200