Theorem ifbieq12d 4499

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  ifcif 4471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3443  df-un 3902  df-if 4472

This theorem is referenced by:  csbif  4528  csbopg  4833  tz7.44-2  8285  tz7.44-3  8286  boxcutc  8777  unxpdomlem1  9092  ttrcltr  9545  updjudhcoinlf  9761  updjudhcoinrg  9762  dfac12lem1  9972  dfac12r  9975  fin23lem12  10160  fin23lem33  10174  ttukeylem3  10340  ttukey2g  10345  xaddval  13030  seqf1olem2  13836  expval  13857  ccatfval  14348  ccatval1  14353  ccatval1OLD  14354  ccatval2  14355  ccatalpha  14370  relexpsucnnr  14808  ruclem1  16012  eucalgval2  16356  setsstruct  16947  ressval  17014  gsumvalx  18430  gsumpropd  18432  gsumpropd2lem  18433  gsumress  18436  mulgval  18773  pmtrfv  19129  xrsdsval  20714  mvrfval  21261  selvfval  21399  marrepeval  21784  marepveval  21789  mdetunilem9  21841  madutpos  21863  madugsum  21864  minmar1eval  21870  symgmatr01lem  21874  symgmatr01  21875  gsummatr01lem3  21878  gsummatr01lem4  21879  gsummatr01  21880  ptcmplem3  23277  xrhmeo  24181  phtpycc  24226  pcovalg  24247  pcocn  24252  pcohtpylem  24254  pcoass  24259  pcorevlem  24261  ovolunlem1a  24732  ovolunlem1  24733  ioombl1  24798  mbfmax  24885  mbfpos  24887  mbfi1fseqlem2  24953  mbfi1fseq  24958  ditgeq1  25084  ditgeq2  25085  ig1pval  25409  cxpval  25891  lgamgulmlem4  26253  lgamgulmlem5  26254  musumsum  26413  muinv  26414  lgsval  26521  gausslemma2dlem1a  26585  gausslemma2dlem2  26587  gausslemma2dlem3  26588  gausslemma2dlem4  26589  vtxval  27479  iedgval  27480  crctcshwlkn0lem2  28285  crctcshwlkn0lem3  28286  crctcshlem4  28294  crctcsh  28298  clwlkclwwlklem2fv1  28468  eucrct2eupth  28718  psgnfzto1stlem  31475  resvval  31630  smatrcl  31852  smatlem  31853  madjusmdetlem2  31884  madjusmdet  31887  ballotlemsv  32582  ballotlemsf1o  32586  plymulx0  32632  mrsubcv  33577  mrsubrn  33580  rdgprc0  33868  dfrdg2  33870  csbrdgg  35556  csbfinxpg  35615  finxpreclem3  35620  poimirlem2  35835  poimirlem23  35856  poimirlem24  35857  poimirlem27  35860  itg2addnclem3  35886  itgaddnclem2  35892  ftc1anclem5  35910  cdleme27b  38587  cdleme29b  38594  cdleme31sn  38599  cdleme31fv  38609  cdleme40v  38688  dihffval  39449  dihfval  39450  dihval  39451  metakunt3  40335  metakunt4  40336  metakunt6  40338  metakunt7  40339  metakunt8  40340  metakunt10  40342  metakunt11  40343  metakunt12  40344  metakunt20  40352  metakunt21  40353  metakunt22  40354  metakunt32  40364  prjspnfv01  40664  prjspner01  40665  prjspner1  40666  aomclem8  41090  mnringvald  42047  icccncfext  43665  dvnxpaek  43720  fourierdlem103  43987  fourierdlem104  43988  ioorrnopn  44083  ioorrnopnxr  44085  hsphoival  44355  sge0hsphoire  44365  hoidmvlelem1  44371  hoidmvlelem2  44372  hoidmvlelem3  44373  hoidmvlelem4  44374  hoidmvlelem5  44375  hoidifhspval3  44395  hspmbllem2  44403  ovolval4  44427  afv2eq12d  44959