Theorem ifbieq12d 4555

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ifcif 4527

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-un 3952  df-if 4528

This theorem is referenced by:  csbif  4584  csbopg  4890  tz7.44-2  8403  tz7.44-3  8404  boxcutc  8931  unxpdomlem1  9246  ttrcltr  9707  updjudhcoinlf  9923  updjudhcoinrg  9924  dfac12lem1  10134  dfac12r  10137  fin23lem12  10322  fin23lem33  10336  ttukeylem3  10502  ttukey2g  10507  xaddval  13198  seqf1olem2  14004  expval  14025  ccatfval  14519  ccatval1  14523  ccatval2  14524  ccatalpha  14539  relexpsucnnr  14968  ruclem1  16170  eucalgval2  16514  setsstruct  17105  ressval  17172  gsumvalx  18591  gsumpropd  18593  gsumpropd2lem  18594  gsumress  18597  mulgval  18948  pmtrfv  19314  xrsdsval  20981  mvrfval  21531  selvfval  21671  marrepeval  22056  marepveval  22061  mdetunilem9  22113  madutpos  22135  madugsum  22136  minmar1eval  22142  symgmatr01lem  22146  symgmatr01  22147  gsummatr01lem3  22150  gsummatr01lem4  22151  gsummatr01  22152  ptcmplem3  23549  xrhmeo  24453  phtpycc  24498  pcovalg  24519  pcocn  24524  pcohtpylem  24526  pcoass  24531  pcorevlem  24533  ovolunlem1a  25004  ovolunlem1  25005  ioombl1  25070  mbfmax  25157  mbfpos  25159  mbfi1fseqlem2  25225  mbfi1fseq  25230  ditgeq1  25356  ditgeq2  25357  ig1pval  25681  cxpval  26163  lgamgulmlem4  26525  lgamgulmlem5  26526  musumsum  26685  muinv  26686  lgsval  26793  gausslemma2dlem1a  26857  gausslemma2dlem2  26859  gausslemma2dlem3  26860  gausslemma2dlem4  26861  vtxval  28249  iedgval  28250  crctcshwlkn0lem2  29054  crctcshwlkn0lem3  29055  crctcshlem4  29063  crctcsh  29067  clwlkclwwlklem2fv1  29237  eucrct2eupth  29487  psgnfzto1stlem  32246  resvval  32429  smatrcl  32764  smatlem  32765  madjusmdetlem2  32796  madjusmdet  32799  ballotlemsv  33496  ballotlemsf1o  33500  plymulx0  33546  mrsubcv  34489  mrsubrn  34492  rdgprc0  34753  dfrdg2  34755  csbrdgg  36198  csbfinxpg  36257  finxpreclem3  36262  poimirlem2  36478  poimirlem23  36499  poimirlem24  36500  poimirlem27  36503  itg2addnclem3  36529  itgaddnclem2  36535  ftc1anclem5  36553  cdleme27b  39227  cdleme29b  39234  cdleme31sn  39239  cdleme31fv  39249  cdleme40v  39328  dihffval  40089  dihfval  40090  dihval  40091  metakunt3  40975  metakunt4  40976  metakunt6  40978  metakunt7  40979  metakunt8  40980  metakunt10  40982  metakunt11  40983  metakunt12  40984  metakunt20  40992  metakunt21  40993  metakunt22  40994  metakunt32  41004  selvvvval  41154  prjspnfv01  41362  prjspner01  41363  prjspner1  41364  aomclem8  41788  mnringvald  42952  icccncfext  44589  dvnxpaek  44644  fourierdlem103  44911  fourierdlem104  44912  ioorrnopn  45007  ioorrnopnxr  45009  hsphoival  45281  sge0hsphoire  45291  hoidmvlelem1  45297  hoidmvlelem2  45298  hoidmvlelem3  45299  hoidmvlelem4  45300  hoidmvlelem5  45301  hoidifhspval3  45321  hspmbllem2  45329  ovolval4  45353  afv2eq12d  45909