Theorem ifbieq12d 4371

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507  ifcif 4344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-un 3828  df-if 4345

This theorem is referenced by:  csbif  4399  csbopg  4691  tz7.44-2  7845  tz7.44-3  7846  boxcutc  8300  unxpdomlem1  8515  updjudhcoinlf  9153  updjudhcoinrg  9154  dfac12lem1  9361  dfac12r  9364  fin23lem12  9549  fin23lem33  9563  ttukeylem3  9729  ttukey2g  9734  xaddval  12431  seqf1olem2  13223  expval  13244  ccatfval  13734  ccatval1  13738  ccatval2  13739  ccatalpha  13754  relexpsucnnr  14243  ruclem1  15442  eucalgval2  15779  setsstruct  16377  ressval  16405  gsumvalx  17750  gsumpropd  17752  gsumpropd2lem  17753  gsumress  17756  mulgval  18027  pmtrfv  18353  mvrfval  19926  xrsdsval  20303  marrepeval  20888  marepveval  20893  mdetunilem9  20945  madutpos  20967  madugsum  20968  minmar1eval  20974  symgmatr01lem  20978  symgmatr01  20979  gsummatr01lem3  20982  gsummatr01lem4  20983  gsummatr01  20984  ptcmplem3  22378  xrhmeo  23265  phtpycc  23310  pcovalg  23331  pcocn  23336  pcohtpylem  23338  pcoass  23343  pcorevlem  23345  ovolunlem1a  23812  ovolunlem1  23813  ioombl1  23878  mbfmax  23965  mbfpos  23967  mbfi1fseqlem2  24032  mbfi1fseq  24037  ditgeq1  24161  ditgeq2  24162  ig1pval  24481  cxpval  24960  lgamgulmlem4  25323  lgamgulmlem5  25324  musumsum  25483  muinv  25484  lgsval  25591  gausslemma2dlem1a  25655  gausslemma2dlem2  25657  gausslemma2dlem3  25658  gausslemma2dlem4  25659  vtxval  26500  iedgval  26501  crctcshwlkn0lem2  27309  crctcshwlkn0lem3  27310  crctcshlem4  27318  crctcsh  27322  clwlkclwwlklem2fv1  27513  eucrct2eupthOLD  27788  eucrct2eupth  27789  resvval  30608  psgnfzto1stlem  30720  smatrcl  30732  smatlem  30733  madjusmdetlem2  30764  madjusmdet  30767  ballotlemsv  31442  ballotlemsf1o  31446  plymulx0  31492  mrsubcv  32306  mrsubrn  32309  rdgprc0  32588  dfrdg2  32590  csbrdgg  34081  csbfinxpg  34139  finxpreclem3  34144  poimirlem2  34364  poimirlem23  34385  poimirlem24  34386  poimirlem27  34389  itg2addnclem3  34415  itgaddnclem2  34421  ftc1anclem5  34441  cdleme27b  36978  cdleme29b  36985  cdleme31sn  36990  cdleme31fv  37000  cdleme40v  37079  dihffval  37840  dihfval  37841  dihval  37842  aomclem8  39086  icccncfext  41625  dvnxpaek  41682  fourierdlem103  41950  fourierdlem104  41951  ioorrnopn  42046  ioorrnopnxr  42048  hsphoival  42317  sge0hsphoire  42327  hoidmvlelem1  42333  hoidmvlelem2  42334  hoidmvlelem3  42335  hoidmvlelem4  42336  hoidmvlelem5  42337  hoidifhspval3  42357  hspmbllem2  42365  ovolval4  42389  afv2eq12d  42845