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 1570  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3903  df-if 4482

This theorem is used by:  csbif  4539  csbopg  4850  tz7.44-2  8393  tz7.44-3  8394  boxcutc  8947  unxpdomlem1  9225  ttrcltr  9695  updjudhcoinlf  9984  updjudhcoinrg  9985  dfac12lem1  10193  dfac12r  10196  fin23lem12  10380  fin23lem33  10394  ttukeylem3  10560  ttukey2g  10565  xaddval  13322  seqf1olem2  14153  expval  14174  ccatfval  14685  ccatval1  14689  ccatval2  14690  ccatalpha  14707  relexpsucnnr  15145  ruclem1  16366  eucalgval2  16718  setsstruct  17315  ressval  17372  gsumvalx  18826  gsumpropd  18828  gsumpropd2lem  18829  gsumress  18832  mulgval  19242  pmtrfv  19627  xrsdsval  21678  mvrfval  22249  selvfval  22389  selvvvval  22412  marrepeval  22839  marepveval  22844  mdetunilem9  22896  madutpos  22918  madugsum  22919  minmar1eval  22925  symgmatr01lem  22929  symgmatr01  22930  gsummatr01lem3  22933  gsummatr01lem4  22934  gsummatr01  22935  ptcmplem3  24334  xrhmeo  25228  phtpycc  25273  pcovalg  25294  pcocn  25299  pcohtpylem  25301  pcoass  25306  pcorevlem  25308  ovolunlem1a  25778  ovolunlem1  25779  ioombl1  25844  mbfmax  25931  mbfpos  25933  mbfi1fseqlem2  25998  mbfi1fseq  26003  ditgeq1  26129  ditgeq2  26130  ig1pval  26455  plyn0mulidp  26565  cxpval  26955  lgamgulmlem4  27322  lgamgulmlem5  27323  musumsum  27482  muinv  27483  lgsval  27591  gausslemma2dlem1a  27655  gausslemma2dlem2  27657  gausslemma2dlem3  27658  gausslemma2dlem4  27659  abssval  28558  expsval  28744  angmgmval  29327  vtxval  29511  iedgval  29512  crctcshwlkn0lem2  30333  crctcshwlkn0lem3  30334  crctcshlem4  30342  crctcsh  30346  clwlkclwwlklem2fv1  30519  eucrct2eupth  30779  ccatws1f1o  33447  psgnfzto1stlem  33594  resvval  33823  esplyfv1  34134  smatrcl  34361  smatlem  34362  madjusmdetlem2  34393  madjusmdet  34396  ballotlemsv  35076  ballotlemsf1o  35080  mrsubcv  36196  mrsubrn  36199  rdgprc0  36477  dfrdg2  36479  ditgeq123dv  36932  cbvditgdavw2  37009  csbrdgg  38172  csbfinxpg  38231  finxpreclem3  38236  poimirlem2  38460  poimirlem23  38481  poimirlem24  38482  poimirlem27  38485  itg2addnclem3  38511  itgaddnclem2  38517  ftc1anclem5  38535  cdleme27b  41345  cdleme29b  41352  cdleme31sn  41357  cdleme31fv  41367  cdleme40v  41446  dihffval  42207  dihfval  42208  dihval  42209  prjspnfv01  43574  prjspner01  43575  prjspner1  43576  aomclem8  44006  mnringvald  45155  icccncfext  46819  dvnxpaek  46874  fourierdlem103  47141  fourierdlem104  47142  ioorrnopn  47237  ioorrnopnxr  47239  hsphoival  47511  sge0hsphoire  47521  hoidmvlelem1  47527  hoidmvlelem2  47528  hoidmvlelem3  47529  hoidmvlelem4  47530  hoidmvlelem5  47531  hoidifhspval3  47551  hspmbllem2  47559  ovolval4  47583  afv2eq12d  48207