Theorem ifbieq12d 4501

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3393  df-v 3435  df-un 3904  df-if 4473

This theorem is referenced by:  csbif  4530  csbopg  4840  tz7.44-2  8320  tz7.44-3  8321  boxcutc  8859  unxpdomlem1  9134  ttrcltr  9600  updjudhcoinlf  9816  updjudhcoinrg  9817  dfac12lem1  10026  dfac12r  10029  fin23lem12  10213  fin23lem33  10227  ttukeylem3  10393  ttukey2g  10398  xaddval  13113  seqf1olem2  13937  expval  13958  ccatfval  14468  ccatval1  14472  ccatval2  14473  ccatalpha  14488  relexpsucnnr  14919  ruclem1  16127  eucalgval2  16479  setsstruct  17074  ressval  17131  gsumvalx  18537  gsumpropd  18539  gsumpropd2lem  18540  gsumress  18543  mulgval  18937  pmtrfv  19318  xrsdsval  21301  mvrfval  21872  selvfval  22003  marrepeval  22432  marepveval  22437  mdetunilem9  22489  madutpos  22511  madugsum  22512  minmar1eval  22518  symgmatr01lem  22522  symgmatr01  22523  gsummatr01lem3  22526  gsummatr01lem4  22527  gsummatr01  22528  ptcmplem3  23923  xrhmeo  24825  phtpycc  24871  pcovalg  24893  pcocn  24898  pcohtpylem  24900  pcoass  24905  pcorevlem  24907  ovolunlem1a  25378  ovolunlem1  25379  ioombl1  25444  mbfmax  25531  mbfpos  25533  mbfi1fseqlem2  25598  mbfi1fseq  25603  ditgeq1  25730  ditgeq2  25731  ig1pval  26062  cxpval  26554  lgamgulmlem4  26923  lgamgulmlem5  26924  musumsum  27083  muinv  27084  lgsval  27193  gausslemma2dlem1a  27257  gausslemma2dlem2  27259  gausslemma2dlem3  27260  gausslemma2dlem4  27261  abssval  28131  expsval  28302  vtxval  28932  iedgval  28933  crctcshwlkn0lem2  29743  crctcshwlkn0lem3  29744  crctcshlem4  29752  crctcsh  29756  clwlkclwwlklem2fv1  29926  eucrct2eupth  30176  ccatws1f1o  32888  psgnfzto1stlem  33037  resvval  33262  esplyfv1  33558  smatrcl  33777  smatlem  33778  madjusmdetlem2  33809  madjusmdet  33812  ballotlemsv  34491  ballotlemsf1o  34495  plymulx0  34528  mrsubcv  35500  mrsubrn  35503  rdgprc0  35784  dfrdg2  35786  ditgeq123dv  36212  cbvditgdavw2  36289  csbrdgg  37320  csbfinxpg  37379  finxpreclem3  37384  poimirlem2  37619  poimirlem23  37640  poimirlem24  37641  poimirlem27  37644  itg2addnclem3  37670  itgaddnclem2  37676  ftc1anclem5  37694  cdleme27b  40364  cdleme29b  40371  cdleme31sn  40376  cdleme31fv  40386  cdleme40v  40465  dihffval  41226  dihfval  41227  dihval  41228  selvvvval  42575  prjspnfv01  42614  prjspner01  42615  prjspner1  42616  aomclem8  43051  mnringvald  44203  icccncfext  45882  dvnxpaek  45937  fourierdlem103  46204  fourierdlem104  46205  ioorrnopn  46300  ioorrnopnxr  46302  hsphoival  46574  sge0hsphoire  46584  hoidmvlelem1  46590  hoidmvlelem2  46591  hoidmvlelem3  46592  hoidmvlelem4  46593  hoidmvlelem5  46594  hoidifhspval3  46614  hspmbllem2  46622  ovolval4  46646  afv2eq12d  47213