Theorem ifbieq12d 4510

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 4151  df-if 4482

This theorem is used by:  csbif  4539  csbopg  4850  tz7.44-2  8415  tz7.44-3  8416  boxcutc  8969  unxpdomlem1  9247  ttrcltr  9717  updjudhcoinlf  10013  updjudhcoinrg  10014  dfac12lem1  10222  dfac12r  10225  fin23lem12  10409  fin23lem33  10423  ttukeylem3  10589  ttukey2g  10594  xaddval  13353  seqf1olem2  14185  expval  14206  ccatfval  14718  ccatval1  14722  ccatval2  14723  ccatalpha  14740  relexpsucnnr  15178  ruclem1  16399  eucalgval2  16756  setsstruct  17354  ressval  17411  gsumvalx  18865  gsumpropd  18867  gsumpropd2lem  18868  gsumress  18871  mulgval  19281  pmtrfv  19666  xrsdsval  21717  mvrfval  22288  selvfval  22428  selvvvval  22451  marrepeval  22878  marepveval  22883  mdetunilem9  22935  madutpos  22957  madugsum  22958  minmar1eval  22964  symgmatr01lem  22968  symgmatr01  22969  gsummatr01lem3  22972  gsummatr01lem4  22973  gsummatr01  22974  ptcmplem3  24373  xrhmeo  25267  phtpycc  25312  pcovalg  25333  pcocn  25338  pcohtpylem  25340  pcoass  25345  pcorevlem  25347  ovolunlem1a  25817  ovolunlem1  25818  ioombl1  25883  mbfmax  25970  mbfpos  25972  mbfi1fseqlem2  26037  mbfi1fseq  26042  ditgeq1  26168  ditgeq2  26169  ig1pval  26494  plyn0mulidp  26602  cxpval  26992  lgamgulmlem4  27359  lgamgulmlem5  27360  musumsum  27519  muinv  27520  lgsval  27628  gausslemma2dlem1a  27692  gausslemma2dlem2  27694  gausslemma2dlem3  27695  gausslemma2dlem4  27696  abssval  28625  expsval  28811  angmgmval  29394  vtxval  29578  iedgval  29579  crctcshwlkn0lem2  30400  crctcshwlkn0lem3  30401  crctcshlem4  30409  crctcsh  30413  clwlkclwwlklem2fv1  30586  eucrct2eupth  30846  ccatws1f1o  33514  psgnfzto1stlem  33661  resvval  33890  esplyfv1  34201  smatrcl  34428  smatlem  34429  madjusmdetlem2  34460  madjusmdet  34463  ballotlemsv  35142  ballotlemsf1o  35146  soinfdom  35717  mrsubcv  36275  mrsubrn  36278  rdgprc0  36555  dfrdg2  36557  ditgeq123dv  37010  cbvditgdavw2  37087  csbrdgg  38253  csbfinxpg  38312  finxpreclem3  38317  poimirlem2  38541  poimirlem23  38562  poimirlem24  38563  poimirlem27  38566  itg2addnclem3  38592  itgaddnclem2  38598  ftc1anclem5  38616  cdleme27b  41426  cdleme29b  41433  cdleme31sn  41438  cdleme31fv  41448  cdleme40v  41527  dihffval  42288  dihfval  42289  dihval  42290  aomclem8  44063  mnringvald  45211  icccncfext  46897  dvnxpaek  46952  fourierdlem103  47219  fourierdlem104  47220  ioorrnopn  47315  ioorrnopnxr  47317  hsphoival  47589  sge0hsphoire  47599  hoidmvlelem1  47605  hoidmvlelem2  47606  hoidmvlelem3  47607  hoidmvlelem4  47608  hoidmvlelem5  47609  hoidifhspval3  47629  hspmbllem2  47637  ovolval4  47661  afv2eq12d  48285