Theorem ifbieq12d 4488

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-un 3893  df-if 4461

This theorem is referenced by:  csbif  4517  csbopg  4823  tz7.44-2  8247  tz7.44-3  8248  boxcutc  8738  unxpdomlem1  9036  ttrcltr  9483  updjudhcoinlf  9699  updjudhcoinrg  9700  dfac12lem1  9908  dfac12r  9911  fin23lem12  10096  fin23lem33  10110  ttukeylem3  10276  ttukey2g  10281  xaddval  12966  seqf1olem2  13772  expval  13793  ccatfval  14285  ccatval1  14290  ccatval1OLD  14291  ccatval2  14292  ccatalpha  14307  relexpsucnnr  14745  ruclem1  15949  eucalgval2  16295  setsstruct  16886  ressval  16953  gsumvalx  18369  gsumpropd  18371  gsumpropd2lem  18372  gsumress  18375  mulgval  18713  pmtrfv  19069  xrsdsval  20651  mvrfval  21198  selvfval  21336  marrepeval  21721  marepveval  21726  mdetunilem9  21778  madutpos  21800  madugsum  21801  minmar1eval  21807  symgmatr01lem  21811  symgmatr01  21812  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  ptcmplem3  23214  xrhmeo  24118  phtpycc  24163  pcovalg  24184  pcocn  24189  pcohtpylem  24191  pcoass  24196  pcorevlem  24198  ovolunlem1a  24669  ovolunlem1  24670  ioombl1  24735  mbfmax  24822  mbfpos  24824  mbfi1fseqlem2  24890  mbfi1fseq  24895  ditgeq1  25021  ditgeq2  25022  ig1pval  25346  cxpval  25828  lgamgulmlem4  26190  lgamgulmlem5  26191  musumsum  26350  muinv  26351  lgsval  26458  gausslemma2dlem1a  26522  gausslemma2dlem2  26524  gausslemma2dlem3  26525  gausslemma2dlem4  26526  vtxval  27379  iedgval  27380  crctcshwlkn0lem2  28185  crctcshwlkn0lem3  28186  crctcshlem4  28194  crctcsh  28198  clwlkclwwlklem2fv1  28368  eucrct2eupth  28618  psgnfzto1stlem  31376  resvval  31535  smatrcl  31755  smatlem  31756  madjusmdetlem2  31787  madjusmdet  31790  ballotlemsv  32485  ballotlemsf1o  32489  plymulx0  32535  mrsubcv  33481  mrsubrn  33484  rdgprc0  33778  dfrdg2  33780  csbrdgg  35509  csbfinxpg  35568  finxpreclem3  35573  poimirlem2  35788  poimirlem23  35809  poimirlem24  35810  poimirlem27  35813  itg2addnclem3  35839  itgaddnclem2  35845  ftc1anclem5  35863  cdleme27b  38389  cdleme29b  38396  cdleme31sn  38401  cdleme31fv  38411  cdleme40v  38490  dihffval  39251  dihfval  39252  dihval  39253  metakunt3  40134  metakunt4  40135  metakunt6  40137  metakunt7  40138  metakunt8  40139  metakunt10  40141  metakunt11  40142  metakunt12  40143  metakunt20  40151  metakunt21  40152  metakunt22  40153  metakunt32  40163  prjspnfv01  40468  prjspner01  40469  prjspner1  40470  aomclem8  40893  mnringvald  41833  icccncfext  43435  dvnxpaek  43490  fourierdlem103  43757  fourierdlem104  43758  ioorrnopn  43853  ioorrnopnxr  43855  hsphoival  44124  sge0hsphoire  44134  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  hoidmvlelem5  44144  hoidifhspval3  44164  hspmbllem2  44172  ovolval4  44196  afv2eq12d  44718