Theorem ifeq1da 4516

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 4504	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4493	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4493	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2767	. . 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 1540  ifcif 4484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-un 3916  df-if 4485

This theorem is referenced by:  ifeq12da  4518  cantnflem1d  9617  cantnflem1  9618  dfac12lem1  10073  xrmaxeq  13115  xrmineq  13116  rexmul  13207  max0add  15252  sumeq2ii  15635  fsumser  15672  ramcl  16976  dmdprdsplitlem  19945  coe1pwmul  22141  scmatscmiddistr  22371  mulmarep1gsum1  22436  maducoeval2  22503  madugsum  22506  madurid  22507  ptcld  23476  ibllem  25641  itgvallem3  25663  iblposlem  25669  iblss2  25683  iblmulc2  25708  cnplimc  25764  limcco  25770  dvexp3  25858  dchrinvcl  27140  lgsval2lem  27194  lgsval4lem  27195  lgsneg  27208  lgsmod  27210  lgsdilem2  27220  rpvmasum2  27399  mrsubrn  35473  ftc1anclem6  37665  ftc1anclem8  37667  fsuppind  42551