Theorem ifbieq12d 4504

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-un 3907  df-if 4476

This theorem is referenced by:  csbif  4533  csbopg  4843  tz7.44-2  8326  tz7.44-3  8327  boxcutc  8865  unxpdomlem1  9140  ttrcltr  9606  updjudhcoinlf  9822  updjudhcoinrg  9823  dfac12lem1  10032  dfac12r  10035  fin23lem12  10219  fin23lem33  10233  ttukeylem3  10399  ttukey2g  10404  xaddval  13119  seqf1olem2  13946  expval  13967  ccatfval  14477  ccatval1  14481  ccatval2  14482  ccatalpha  14498  relexpsucnnr  14929  ruclem1  16137  eucalgval2  16489  setsstruct  17084  ressval  17141  gsumvalx  18581  gsumpropd  18583  gsumpropd2lem  18584  gsumress  18587  mulgval  18981  pmtrfv  19362  xrsdsval  21345  mvrfval  21916  selvfval  22047  marrepeval  22476  marepveval  22481  mdetunilem9  22533  madutpos  22555  madugsum  22556  minmar1eval  22562  symgmatr01lem  22566  symgmatr01  22567  gsummatr01lem3  22570  gsummatr01lem4  22571  gsummatr01  22572  ptcmplem3  23967  xrhmeo  24869  phtpycc  24915  pcovalg  24937  pcocn  24942  pcohtpylem  24944  pcoass  24949  pcorevlem  24951  ovolunlem1a  25422  ovolunlem1  25423  ioombl1  25488  mbfmax  25575  mbfpos  25577  mbfi1fseqlem2  25642  mbfi1fseq  25647  ditgeq1  25774  ditgeq2  25775  ig1pval  26106  cxpval  26598  lgamgulmlem4  26967  lgamgulmlem5  26968  musumsum  27127  muinv  27128  lgsval  27237  gausslemma2dlem1a  27301  gausslemma2dlem2  27303  gausslemma2dlem3  27304  gausslemma2dlem4  27305  abssval  28175  expsval  28346  vtxval  28976  iedgval  28977  crctcshwlkn0lem2  29787  crctcshwlkn0lem3  29788  crctcshlem4  29796  crctcsh  29800  clwlkclwwlklem2fv1  29970  eucrct2eupth  30220  ccatws1f1o  32927  psgnfzto1stlem  33064  resvval  33289  esplyfv1  33585  smatrcl  33804  smatlem  33805  madjusmdetlem2  33836  madjusmdet  33839  ballotlemsv  34518  ballotlemsf1o  34522  plymulx0  34555  mrsubcv  35542  mrsubrn  35545  rdgprc0  35826  dfrdg2  35828  ditgeq123dv  36254  cbvditgdavw2  36331  csbrdgg  37362  csbfinxpg  37421  finxpreclem3  37426  poimirlem2  37661  poimirlem23  37682  poimirlem24  37683  poimirlem27  37686  itg2addnclem3  37712  itgaddnclem2  37718  ftc1anclem5  37736  cdleme27b  40406  cdleme29b  40413  cdleme31sn  40418  cdleme31fv  40428  cdleme40v  40507  dihffval  41268  dihfval  41269  dihval  41270  selvvvval  42617  prjspnfv01  42656  prjspner01  42657  prjspner1  42658  aomclem8  43093  mnringvald  44245  icccncfext  45924  dvnxpaek  45979  fourierdlem103  46246  fourierdlem104  46247  ioorrnopn  46342  ioorrnopnxr  46344  hsphoival  46616  sge0hsphoire  46626  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem4  46635  hoidmvlelem5  46636  hoidifhspval3  46656  hspmbllem2  46664  ovolval4  46688  afv2eq12d  47245