Theorem ifbieq12d 4510

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4481

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-un 3908  df-if 4482

This theorem is referenced by:  csbif  4539  csbopg  4849  tz7.44-2  8348  tz7.44-3  8349  boxcutc  8891  unxpdomlem1  9168  ttrcltr  9637  updjudhcoinlf  9856  updjudhcoinrg  9857  dfac12lem1  10066  dfac12r  10069  fin23lem12  10253  fin23lem33  10267  ttukeylem3  10433  ttukey2g  10438  xaddval  13150  seqf1olem2  13977  expval  13998  ccatfval  14508  ccatval1  14512  ccatval2  14513  ccatalpha  14529  relexpsucnnr  14960  ruclem1  16168  eucalgval2  16520  setsstruct  17115  ressval  17172  gsumvalx  18613  gsumpropd  18615  gsumpropd2lem  18616  gsumress  18619  mulgval  19013  pmtrfv  19393  xrsdsval  21377  mvrfval  21948  selvfval  22089  marrepeval  22519  marepveval  22524  mdetunilem9  22576  madutpos  22598  madugsum  22599  minmar1eval  22605  symgmatr01lem  22609  symgmatr01  22610  gsummatr01lem3  22613  gsummatr01lem4  22614  gsummatr01  22615  ptcmplem3  24010  xrhmeo  24912  phtpycc  24958  pcovalg  24980  pcocn  24985  pcohtpylem  24987  pcoass  24992  pcorevlem  24994  ovolunlem1a  25465  ovolunlem1  25466  ioombl1  25531  mbfmax  25618  mbfpos  25620  mbfi1fseqlem2  25685  mbfi1fseq  25690  ditgeq1  25817  ditgeq2  25818  ig1pval  26149  cxpval  26641  lgamgulmlem4  27010  lgamgulmlem5  27011  musumsum  27170  muinv  27171  lgsval  27280  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem3  27347  gausslemma2dlem4  27348  abssval  28247  expsval  28433  vtxval  29085  iedgval  29086  crctcshwlkn0lem2  29896  crctcshwlkn0lem3  29897  crctcshlem4  29905  crctcsh  29909  clwlkclwwlklem2fv1  30082  eucrct2eupth  30332  ccatws1f1o  33043  psgnfzto1stlem  33193  resvval  33421  esplyfv1  33745  smatrcl  33973  smatlem  33974  madjusmdetlem2  34005  madjusmdet  34008  ballotlemsv  34687  ballotlemsf1o  34691  plymulx0  34724  mrsubcv  35723  mrsubrn  35726  rdgprc0  36004  dfrdg2  36006  ditgeq123dv  36434  cbvditgdavw2  36511  csbrdgg  37578  csbfinxpg  37637  finxpreclem3  37642  poimirlem2  37867  poimirlem23  37888  poimirlem24  37889  poimirlem27  37892  itg2addnclem3  37918  itgaddnclem2  37924  ftc1anclem5  37942  cdleme27b  40738  cdleme29b  40745  cdleme31sn  40750  cdleme31fv  40760  cdleme40v  40839  dihffval  41600  dihfval  41601  dihval  41602  selvvvval  42937  prjspnfv01  42976  prjspner01  42977  prjspner1  42978  aomclem8  43412  mnringvald  44563  icccncfext  46239  dvnxpaek  46294  fourierdlem103  46561  fourierdlem104  46562  ioorrnopn  46657  ioorrnopnxr  46659  hsphoival  46931  sge0hsphoire  46941  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem4  46950  hoidmvlelem5  46951  hoidifhspval3  46971  hspmbllem2  46979  ovolval4  47003  afv2eq12d  47569