Theorem ifbieq12d 4514

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-un 3907  df-if 4486

This theorem is used by:  csbif  4543  csbopg  4854  tz7.44-2  8399  tz7.44-3  8400  boxcutc  8951  unxpdomlem1  9229  ttrcltr  9698  updjudhcoinlf  9940  updjudhcoinrg  9941  dfac12lem1  10149  dfac12r  10152  fin23lem12  10336  fin23lem33  10350  ttukeylem3  10516  ttukey2g  10521  xaddval  13277  seqf1olem2  14108  expval  14129  ccatfval  14640  ccatval1  14644  ccatval2  14645  ccatalpha  14662  relexpsucnnr  15100  ruclem1  16323  eucalgval2  16675  setsstruct  17272  ressval  17329  gsumvalx  18780  gsumpropd  18782  gsumpropd2lem  18783  gsumress  18786  mulgval  19195  pmtrfv  19580  xrsdsval  21625  mvrfval  22196  selvfval  22336  selvvvval  22359  marrepeval  22786  marepveval  22791  mdetunilem9  22843  madutpos  22865  madugsum  22866  minmar1eval  22872  symgmatr01lem  22876  symgmatr01  22877  gsummatr01lem3  22880  gsummatr01lem4  22881  gsummatr01  22882  ptcmplem3  24281  xrhmeo  25175  phtpycc  25220  pcovalg  25241  pcocn  25246  pcohtpylem  25248  pcoass  25253  pcorevlem  25255  ovolunlem1a  25725  ovolunlem1  25726  ioombl1  25791  mbfmax  25878  mbfpos  25880  mbfi1fseqlem2  25945  mbfi1fseq  25950  ditgeq1  26077  ditgeq2  26078  ig1pval  26403  plyn0mulidp  26512  cxpval  26899  lgamgulmlem4  27266  lgamgulmlem5  27267  musumsum  27426  muinv  27427  lgsval  27535  gausslemma2dlem1a  27599  gausslemma2dlem2  27601  gausslemma2dlem3  27602  gausslemma2dlem4  27603  abssval  28502  expsval  28688  vtxval  29443  iedgval  29444  crctcshwlkn0lem2  30265  crctcshwlkn0lem3  30266  crctcshlem4  30274  crctcsh  30278  clwlkclwwlklem2fv1  30451  eucrct2eupth  30711  ccatws1f1o  33380  psgnfzto1stlem  33527  resvval  33756  esplyfv1  34066  smatrcl  34293  smatlem  34294  madjusmdetlem2  34325  madjusmdet  34328  ballotlemsv  35008  ballotlemsf1o  35012  mrsubcv  36076  mrsubrn  36079  rdgprc0  36357  dfrdg2  36359  ditgeq123dv  36828  cbvditgdavw2  36905  csbrdgg  38070  csbfinxpg  38129  finxpreclem3  38134  poimirlem2  38358  poimirlem23  38379  poimirlem24  38380  poimirlem27  38383  itg2addnclem3  38409  itgaddnclem2  38415  ftc1anclem5  38433  cdleme27b  41228  cdleme29b  41235  cdleme31sn  41240  cdleme31fv  41250  cdleme40v  41329  dihffval  42090  dihfval  42091  dihval  42092  prjspnfv01  43457  prjspner01  43458  prjspner1  43459  aomclem8  43889  mnringvald  45038  icccncfext  46702  dvnxpaek  46757  fourierdlem103  47024  fourierdlem104  47025  ioorrnopn  47120  ioorrnopnxr  47122  hsphoival  47394  sge0hsphoire  47404  hoidmvlelem1  47410  hoidmvlelem2  47411  hoidmvlelem3  47412  hoidmvlelem4  47413  hoidmvlelem5  47414  hoidifhspval3  47434  hspmbllem2  47442  ovolval4  47466  afv2eq12d  48090