Theorem ifbieq12d 4503

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-un 3903  df-if 4475

This theorem is referenced by:  csbif  4532  csbopg  4842  tz7.44-2  8332  tz7.44-3  8333  boxcutc  8871  unxpdomlem1  9147  ttrcltr  9613  updjudhcoinlf  9832  updjudhcoinrg  9833  dfac12lem1  10042  dfac12r  10045  fin23lem12  10229  fin23lem33  10243  ttukeylem3  10409  ttukey2g  10414  xaddval  13124  seqf1olem2  13951  expval  13972  ccatfval  14482  ccatval1  14486  ccatval2  14487  ccatalpha  14503  relexpsucnnr  14934  ruclem1  16142  eucalgval2  16494  setsstruct  17089  ressval  17146  gsumvalx  18586  gsumpropd  18588  gsumpropd2lem  18589  gsumress  18592  mulgval  18986  pmtrfv  19366  xrsdsval  21349  mvrfval  21919  selvfval  22050  marrepeval  22479  marepveval  22484  mdetunilem9  22536  madutpos  22558  madugsum  22559  minmar1eval  22565  symgmatr01lem  22569  symgmatr01  22570  gsummatr01lem3  22573  gsummatr01lem4  22574  gsummatr01  22575  ptcmplem3  23970  xrhmeo  24872  phtpycc  24918  pcovalg  24940  pcocn  24945  pcohtpylem  24947  pcoass  24952  pcorevlem  24954  ovolunlem1a  25425  ovolunlem1  25426  ioombl1  25491  mbfmax  25578  mbfpos  25580  mbfi1fseqlem2  25645  mbfi1fseq  25650  ditgeq1  25777  ditgeq2  25778  ig1pval  26109  cxpval  26601  lgamgulmlem4  26970  lgamgulmlem5  26971  musumsum  27130  muinv  27131  lgsval  27240  gausslemma2dlem1a  27304  gausslemma2dlem2  27306  gausslemma2dlem3  27307  gausslemma2dlem4  27308  abssval  28178  expsval  28349  vtxval  28980  iedgval  28981  crctcshwlkn0lem2  29791  crctcshwlkn0lem3  29792  crctcshlem4  29800  crctcsh  29804  clwlkclwwlklem2fv1  29977  eucrct2eupth  30227  ccatws1f1o  32939  psgnfzto1stlem  33076  resvval  33301  esplyfv1  33609  smatrcl  33830  smatlem  33831  madjusmdetlem2  33862  madjusmdet  33865  ballotlemsv  34544  ballotlemsf1o  34548  plymulx0  34581  mrsubcv  35575  mrsubrn  35578  rdgprc0  35856  dfrdg2  35858  ditgeq123dv  36286  cbvditgdavw2  36363  csbrdgg  37394  csbfinxpg  37453  finxpreclem3  37458  poimirlem2  37682  poimirlem23  37703  poimirlem24  37704  poimirlem27  37707  itg2addnclem3  37733  itgaddnclem2  37739  ftc1anclem5  37757  cdleme27b  40487  cdleme29b  40494  cdleme31sn  40499  cdleme31fv  40509  cdleme40v  40588  dihffval  41349  dihfval  41350  dihval  41351  selvvvval  42703  prjspnfv01  42742  prjspner01  42743  prjspner1  42744  aomclem8  43178  mnringvald  44330  icccncfext  46009  dvnxpaek  46064  fourierdlem103  46331  fourierdlem104  46332  ioorrnopn  46427  ioorrnopnxr  46429  hsphoival  46701  sge0hsphoire  46711  hoidmvlelem1  46717  hoidmvlelem2  46718  hoidmvlelem3  46719  hoidmvlelem4  46720  hoidmvlelem5  46721  hoidifhspval3  46741  hspmbllem2  46749  ovolval4  46773  afv2eq12d  47339