Theorem ifbieq12d 4496

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4467

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-if 4468

This theorem is referenced by:  csbif  4525  csbopg  4835  tz7.44-2  8339  tz7.44-3  8340  boxcutc  8882  unxpdomlem1  9159  ttrcltr  9628  updjudhcoinlf  9847  updjudhcoinrg  9848  dfac12lem1  10057  dfac12r  10060  fin23lem12  10244  fin23lem33  10258  ttukeylem3  10424  ttukey2g  10429  xaddval  13166  seqf1olem2  13995  expval  14016  ccatfval  14526  ccatval1  14530  ccatval2  14531  ccatalpha  14547  relexpsucnnr  14978  ruclem1  16189  eucalgval2  16541  setsstruct  17137  ressval  17194  gsumvalx  18635  gsumpropd  18637  gsumpropd2lem  18638  gsumress  18641  mulgval  19038  pmtrfv  19418  xrsdsval  21400  mvrfval  21969  selvfval  22110  marrepeval  22538  marepveval  22543  mdetunilem9  22595  madutpos  22617  madugsum  22618  minmar1eval  22624  symgmatr01lem  22628  symgmatr01  22629  gsummatr01lem3  22632  gsummatr01lem4  22633  gsummatr01  22634  ptcmplem3  24029  xrhmeo  24923  phtpycc  24968  pcovalg  24989  pcocn  24994  pcohtpylem  24996  pcoass  25001  pcorevlem  25003  ovolunlem1a  25473  ovolunlem1  25474  ioombl1  25539  mbfmax  25626  mbfpos  25628  mbfi1fseqlem2  25693  mbfi1fseq  25698  ditgeq1  25825  ditgeq2  25826  ig1pval  26151  cxpval  26641  lgamgulmlem4  27009  lgamgulmlem5  27010  musumsum  27169  muinv  27170  lgsval  27278  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  gausslemma2dlem3  27345  gausslemma2dlem4  27346  abssval  28245  expsval  28431  vtxval  29083  iedgval  29084  crctcshwlkn0lem2  29894  crctcshwlkn0lem3  29895  crctcshlem4  29903  crctcsh  29907  clwlkclwwlklem2fv1  30080  eucrct2eupth  30330  ccatws1f1o  33026  psgnfzto1stlem  33176  resvval  33404  esplyfv1  33728  smatrcl  33956  smatlem  33957  madjusmdetlem2  33988  madjusmdet  33991  ballotlemsv  34670  ballotlemsf1o  34674  plymulx0  34707  mrsubcv  35708  mrsubrn  35711  rdgprc0  35989  dfrdg2  35991  ditgeq123dv  36419  cbvditgdavw2  36496  csbrdgg  37659  csbfinxpg  37718  finxpreclem3  37723  poimirlem2  37957  poimirlem23  37978  poimirlem24  37979  poimirlem27  37982  itg2addnclem3  38008  itgaddnclem2  38014  ftc1anclem5  38032  cdleme27b  40828  cdleme29b  40835  cdleme31sn  40840  cdleme31fv  40850  cdleme40v  40929  dihffval  41690  dihfval  41691  dihval  41692  selvvvval  43032  prjspnfv01  43071  prjspner01  43072  prjspner1  43073  aomclem8  43507  mnringvald  44658  icccncfext  46333  dvnxpaek  46388  fourierdlem103  46655  fourierdlem104  46656  ioorrnopn  46751  ioorrnopnxr  46753  hsphoival  47025  sge0hsphoire  47035  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hoidmvlelem5  47045  hoidifhspval3  47065  hspmbllem2  47073  ovolval4  47097  afv2eq12d  47675