Theorem ifeq1da 4508

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 4496	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4485	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4485	. . . 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 4476

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 3395  df-v 3438  df-un 3908  df-if 4477

This theorem is referenced by:  ifeq12da  4510  cantnflem1d  9584  cantnflem1  9585  dfac12lem1  10038  xrmaxeq  13081  xrmineq  13082  rexmul  13173  max0add  15217  sumeq2ii  15600  fsumser  15637  ramcl  16941  dmdprdsplitlem  19918  coe1pwmul  22163  scmatscmiddistr  22393  mulmarep1gsum1  22458  maducoeval2  22525  madugsum  22528  madurid  22529  ptcld  23498  ibllem  25663  itgvallem3  25685  iblposlem  25691  iblss2  25705  iblmulc2  25730  cnplimc  25786  limcco  25792  dvexp3  25880  dchrinvcl  27162  lgsval2lem  27216  lgsval4lem  27217  lgsneg  27230  lgsmod  27232  lgsdilem2  27242  rpvmasum2  27421  mrsubrn  35486  ftc1anclem6  37678  ftc1anclem8  37680  fsuppind  42563