Theorem ifbieq12d 4484

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-if 4457

This theorem is referenced by:  csbif  4513  csbopg  4819  tz7.44-2  8209  tz7.44-3  8210  boxcutc  8687  unxpdomlem1  8956  updjudhcoinlf  9621  updjudhcoinrg  9622  dfac12lem1  9830  dfac12r  9833  fin23lem12  10018  fin23lem33  10032  ttukeylem3  10198  ttukey2g  10203  xaddval  12886  seqf1olem2  13691  expval  13712  ccatfval  14204  ccatval1  14209  ccatval1OLD  14210  ccatval2  14211  ccatalpha  14226  relexpsucnnr  14664  ruclem1  15868  eucalgval2  16214  setsstruct  16805  ressval  16870  gsumvalx  18275  gsumpropd  18277  gsumpropd2lem  18278  gsumress  18281  mulgval  18619  pmtrfv  18975  xrsdsval  20554  mvrfval  21099  selvfval  21237  marrepeval  21620  marepveval  21625  mdetunilem9  21677  madutpos  21699  madugsum  21700  minmar1eval  21706  symgmatr01lem  21710  symgmatr01  21711  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  ptcmplem3  23113  xrhmeo  24015  phtpycc  24060  pcovalg  24081  pcocn  24086  pcohtpylem  24088  pcoass  24093  pcorevlem  24095  ovolunlem1a  24565  ovolunlem1  24566  ioombl1  24631  mbfmax  24718  mbfpos  24720  mbfi1fseqlem2  24786  mbfi1fseq  24791  ditgeq1  24917  ditgeq2  24918  ig1pval  25242  cxpval  25724  lgamgulmlem4  26086  lgamgulmlem5  26087  musumsum  26246  muinv  26247  lgsval  26354  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  gausslemma2dlem3  26421  gausslemma2dlem4  26422  vtxval  27273  iedgval  27274  crctcshwlkn0lem2  28077  crctcshwlkn0lem3  28078  crctcshlem4  28086  crctcsh  28090  clwlkclwwlklem2fv1  28260  eucrct2eupth  28510  psgnfzto1stlem  31269  resvval  31428  smatrcl  31648  smatlem  31649  madjusmdetlem2  31680  madjusmdet  31683  ballotlemsv  32376  ballotlemsf1o  32380  plymulx0  32426  mrsubcv  33372  mrsubrn  33375  rdgprc0  33675  dfrdg2  33677  ttrcltr  33702  csbrdgg  35427  csbfinxpg  35486  finxpreclem3  35491  poimirlem2  35706  poimirlem23  35727  poimirlem24  35728  poimirlem27  35731  itg2addnclem3  35757  itgaddnclem2  35763  ftc1anclem5  35781  cdleme27b  38309  cdleme29b  38316  cdleme31sn  38321  cdleme31fv  38331  cdleme40v  38410  dihffval  39171  dihfval  39172  dihval  39173  metakunt3  40055  metakunt4  40056  metakunt6  40058  metakunt7  40059  metakunt8  40060  metakunt10  40062  metakunt11  40063  metakunt12  40064  metakunt20  40072  metakunt21  40073  metakunt22  40074  metakunt32  40084  prjspnfv01  40382  prjspner01  40383  prjspner1  40384  aomclem8  40802  mnringvald  41715  icccncfext  43318  dvnxpaek  43373  fourierdlem103  43640  fourierdlem104  43641  ioorrnopn  43736  ioorrnopnxr  43738  hsphoival  44007  sge0hsphoire  44017  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvlelem5  44027  hoidifhspval3  44047  hspmbllem2  44055  ovolval4  44079  afv2eq12d  44594