Theorem ifbieq12d 4556

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-un 3953  df-if 4529

This theorem is referenced by:  csbif  4585  csbopg  4891  tz7.44-2  8409  tz7.44-3  8410  boxcutc  8937  unxpdomlem1  9252  ttrcltr  9713  updjudhcoinlf  9929  updjudhcoinrg  9930  dfac12lem1  10140  dfac12r  10143  fin23lem12  10328  fin23lem33  10342  ttukeylem3  10508  ttukey2g  10513  xaddval  13204  seqf1olem2  14010  expval  14031  ccatfval  14525  ccatval1  14529  ccatval2  14530  ccatalpha  14545  relexpsucnnr  14974  ruclem1  16176  eucalgval2  16520  setsstruct  17111  ressval  17178  gsumvalx  18597  gsumpropd  18599  gsumpropd2lem  18600  gsumress  18603  mulgval  18956  pmtrfv  19322  xrsdsval  20995  mvrfval  21546  selvfval  21686  marrepeval  22072  marepveval  22077  mdetunilem9  22129  madutpos  22151  madugsum  22152  minmar1eval  22158  symgmatr01lem  22162  symgmatr01  22163  gsummatr01lem3  22166  gsummatr01lem4  22167  gsummatr01  22168  ptcmplem3  23565  xrhmeo  24469  phtpycc  24514  pcovalg  24535  pcocn  24540  pcohtpylem  24542  pcoass  24547  pcorevlem  24549  ovolunlem1a  25020  ovolunlem1  25021  ioombl1  25086  mbfmax  25173  mbfpos  25175  mbfi1fseqlem2  25241  mbfi1fseq  25246  ditgeq1  25372  ditgeq2  25373  ig1pval  25697  cxpval  26179  lgamgulmlem4  26543  lgamgulmlem5  26544  musumsum  26703  muinv  26704  lgsval  26811  gausslemma2dlem1a  26875  gausslemma2dlem2  26877  gausslemma2dlem3  26878  gausslemma2dlem4  26879  vtxval  28298  iedgval  28299  crctcshwlkn0lem2  29103  crctcshwlkn0lem3  29104  crctcshlem4  29112  crctcsh  29116  clwlkclwwlklem2fv1  29286  eucrct2eupth  29536  psgnfzto1stlem  32300  resvval  32482  smatrcl  32845  smatlem  32846  madjusmdetlem2  32877  madjusmdet  32880  ballotlemsv  33577  ballotlemsf1o  33581  plymulx0  33627  mrsubcv  34570  mrsubrn  34573  rdgprc0  34834  dfrdg2  34836  csbrdgg  36296  csbfinxpg  36355  finxpreclem3  36360  poimirlem2  36576  poimirlem23  36597  poimirlem24  36598  poimirlem27  36601  itg2addnclem3  36627  itgaddnclem2  36633  ftc1anclem5  36651  cdleme27b  39325  cdleme29b  39332  cdleme31sn  39337  cdleme31fv  39347  cdleme40v  39426  dihffval  40187  dihfval  40188  dihval  40189  metakunt3  41073  metakunt4  41074  metakunt6  41076  metakunt7  41077  metakunt8  41078  metakunt10  41080  metakunt11  41081  metakunt12  41082  metakunt20  41090  metakunt21  41091  metakunt22  41092  metakunt32  41102  selvvvval  41239  prjspnfv01  41448  prjspner01  41449  prjspner1  41450  aomclem8  41885  mnringvald  43049  icccncfext  44682  dvnxpaek  44737  fourierdlem103  45004  fourierdlem104  45005  ioorrnopn  45100  ioorrnopnxr  45102  hsphoival  45374  sge0hsphoire  45384  hoidmvlelem1  45390  hoidmvlelem2  45391  hoidmvlelem3  45392  hoidmvlelem4  45393  hoidmvlelem5  45394  hoidifhspval3  45414  hspmbllem2  45422  ovolval4  45446  afv2eq12d  46002