Theorem ifeq1da 4509

Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypothesis

Ref	Expression
ifeq1da.1	⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifeq1da	⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Proof of Theorem ifeq1da

Step	Hyp	Ref	Expression
1		ifeq1da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵)
2	1	ifeq1d 4497	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4486	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4486	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2772	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 481	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 812	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-un 3904  df-if 4478

This theorem is referenced by:  ifeq12da  4511  cantnflem1d  9595  cantnflem1  9596  dfac12lem1  10052  xrmaxeq  13092  xrmineq  13093  rexmul  13184  max0add  15231  sumeq2ii  15614  fsumser  15651  ramcl  16955  dmdprdsplitlem  19966  coe1pwmul  22219  scmatscmiddistr  22450  mulmarep1gsum1  22515  maducoeval2  22582  madugsum  22585  madurid  22586  ptcld  23555  ibllem  25719  itgvallem3  25741  iblposlem  25747  iblss2  25761  iblmulc2  25786  cnplimc  25842  limcco  25848  dvexp3  25936  dchrinvcl  27218  lgsval2lem  27272  lgsval4lem  27273  lgsneg  27286  lgsmod  27288  lgsdilem2  27298  rpvmasum2  27477  esplyind  33680  mrsubrn  35656  ftc1anclem6  37838  ftc1anclem8  37840  fsuppind  42775