Theorem ifbieq12d 4113

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-un 3579  df-if 4087

This theorem is referenced by:  csbif  4138  csbopg  4420  tz7.44-2  7503  tz7.44-3  7504  boxcutc  7951  unxpdomlem1  8164  dfac12lem1  8965  dfac12r  8968  fin23lem12  9153  fin23lem33  9167  ttukeylem3  9333  ttukey2g  9338  xaddval  12054  seqf1olem2  12841  expval  12862  ccatfval  13358  ccatval1  13361  ccatval2  13362  ccatalpha  13375  relexpsucnnr  13765  ruclem1  14960  eucalgval2  15294  setsstruct  15898  ressval  15927  gsumvalx  17270  gsumpropd  17272  gsumpropd2lem  17273  gsumress  17276  mulgval  17543  pmtrfv  17872  mvrfval  19420  xrsdsval  19790  marrepeval  20369  marepveval  20374  mdetunilem9  20426  madutpos  20448  madugsum  20449  minmar1eval  20455  symgmatr01lem  20459  symgmatr01  20460  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  ptcmplem3  21858  xrhmeo  22745  phtpycc  22790  pcovalg  22812  pcocn  22817  pcohtpylem  22819  pcoass  22824  pcorevlem  22826  ovolunlem1a  23264  ovolunlem1  23265  ioombl1  23330  mbfmax  23416  mbfpos  23418  mbfi1fseqlem2  23483  mbfi1fseq  23488  ditgeq1  23612  ditgeq2  23613  ig1pval  23932  cxpval  24410  lgamgulmlem4  24758  lgamgulmlem5  24759  musumsum  24918  muinv  24919  lgsval  25026  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  gausslemma2dlem3  25093  gausslemma2dlem4  25094  vtxval  25878  iedgval  25879  vtxvalOLD  25880  iedgvalOLD  25881  crctcshwlkn0lem2  26703  crctcshwlkn0lem3  26704  crctcshlem4  26712  crctcsh  26716  clwlkclwwlklem2fv1  26896  eucrct2eupth  27105  resvval  29827  psgnfzto1stlem  29850  smatrcl  29862  smatlem  29863  madjusmdetlem2  29894  madjusmdet  29897  ballotlemsv  30571  ballotlemsf1o  30575  plymulx0  30624  mrsubcv  31407  mrsubrn  31410  rdgprc0  31699  dfrdg2  31701  csbrdgg  33175  csbfinxpg  33225  finxpreclem3  33230  poimirlem2  33411  poimirlem23  33432  poimirlem24  33433  poimirlem27  33436  itg2addnclem3  33463  itgaddnclem2  33469  ftc1anclem5  33489  cdleme27b  35656  cdleme29b  35663  cdleme31sn  35668  cdleme31fv  35678  cdleme40v  35757  dihffval  36519  dihfval  36520  dihval  36521  aomclem8  37631  ifeq123d  39207  icccncfext  40100  dvnxpaek  40157  ioorrnopn  40525  ioorrnopnxr  40527  hsphoival  40793  sge0hsphoire  40803  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoidmvlelem5  40813  hoidifhspval3  40833  hspmbllem2  40841  ovolval4  40865