Theorem ifbieq12d 4511

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562  ifcif 4482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-un 3911  df-if 4483

This theorem is referenced by:  csbif  4540  csbopg  4851  tz7.44-2  8380  tz7.44-3  8381  boxcutc  8925  unxpdomlem1  9202  ttrcltr  9673  updjudhcoinlf  9892  updjudhcoinrg  9893  dfac12lem1  10102  dfac12r  10105  fin23lem12  10290  fin23lem33  10304  ttukeylem3  10470  ttukey2g  10475  xaddval  13228  seqf1olem2  14057  expval  14078  ccatfval  14588  ccatval1  14592  ccatval2  14593  ccatalpha  14609  relexpsucnnr  15040  ruclem1  16265  eucalgval2  16617  setsstruct  17214  ressval  17271  gsumvalx  18712  gsumpropd  18714  gsumpropd2lem  18715  gsumress  18718  mulgval  19115  pmtrfv  19494  xrsdsval  21465  mvrfval  22034  selvfval  22174  selvvvval  22197  marrepeval  22625  marepveval  22630  mdetunilem9  22682  madutpos  22704  madugsum  22705  minmar1eval  22711  symgmatr01lem  22715  symgmatr01  22716  gsummatr01lem3  22719  gsummatr01lem4  22720  gsummatr01  22721  ptcmplem3  24116  xrhmeo  25010  phtpycc  25055  pcovalg  25076  pcocn  25081  pcohtpylem  25083  pcoass  25088  pcorevlem  25090  ovolunlem1a  25560  ovolunlem1  25561  ioombl1  25626  mbfmax  25713  mbfpos  25715  mbfi1fseqlem2  25780  mbfi1fseq  25785  ditgeq1  25912  ditgeq2  25913  ig1pval  26238  plyn0mulidp  26347  cxpval  26731  lgamgulmlem4  27098  lgamgulmlem5  27099  musumsum  27258  muinv  27259  lgsval  27367  gausslemma2dlem1a  27431  gausslemma2dlem2  27433  gausslemma2dlem3  27434  gausslemma2dlem4  27435  abssval  28334  expsval  28520  vtxval  29203  iedgval  29204  crctcshwlkn0lem2  30013  crctcshwlkn0lem3  30014  crctcshlem4  30022  crctcsh  30026  clwlkclwwlklem2fv1  30199  eucrct2eupth  30449  ccatws1f1o  33131  psgnfzto1stlem  33282  resvval  33517  esplyfv1  33868  smatrcl  34095  smatlem  34096  madjusmdetlem2  34127  madjusmdet  34130  ballotlemsv  34809  ballotlemsf1o  34813  mrsubcv  35865  mrsubrn  35868  rdgprc0  36146  dfrdg2  36148  ditgeq123dv  36586  cbvditgdavw2  36663  csbrdgg  37828  csbfinxpg  37887  finxpreclem3  37892  poimirlem2  38126  poimirlem23  38147  poimirlem24  38148  poimirlem27  38151  itg2addnclem3  38177  itgaddnclem2  38183  ftc1anclem5  38201  cdleme27b  40997  cdleme29b  41004  cdleme31sn  41009  cdleme31fv  41019  cdleme40v  41098  dihffval  41859  dihfval  41860  dihval  41861  prjspnfv01  43211  prjspner01  43212  prjspner1  43213  aomclem8  43643  mnringvald  44794  icccncfext  46466  dvnxpaek  46521  fourierdlem103  46788  fourierdlem104  46789  ioorrnopn  46884  ioorrnopnxr  46886  hsphoival  47158  sge0hsphoire  47168  hoidmvlelem1  47174  hoidmvlelem2  47175  hoidmvlelem3  47176  hoidmvlelem4  47177  hoidmvlelem5  47178  hoidifhspval3  47198  hspmbllem2  47206  ovolval4  47230  afv2eq12d  47814