Theorem ifeq1da 4557

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 4545	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4534	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4534	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2780	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 481	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 813	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540  ifcif 4525

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-if 4526

This theorem is referenced by:  ifeq12da  4559  cantnflem1d  9728  cantnflem1  9729  dfac12lem1  10184  xrmaxeq  13221  xrmineq  13222  rexmul  13313  max0add  15349  sumeq2ii  15729  fsumser  15766  ramcl  17067  dmdprdsplitlem  20057  coe1pwmul  22282  scmatscmiddistr  22514  mulmarep1gsum1  22579  maducoeval2  22646  madugsum  22649  madurid  22650  ptcld  23621  ibllem  25799  itgvallem3  25821  iblposlem  25827  iblss2  25841  iblmulc2  25866  cnplimc  25922  limcco  25928  dvexp3  26016  dchrinvcl  27297  lgsval2lem  27351  lgsval4lem  27352  lgsneg  27365  lgsmod  27367  lgsdilem2  27377  rpvmasum2  27556  mrsubrn  35518  ftc1anclem6  37705  ftc1anclem8  37707  fsuppind  42600