Theorem ifeq1da 4524

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 4512	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4501	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4501	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2807	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 486	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 824	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1567  ifcif 4492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-un 3918  df-if 4493

This theorem is referenced by:  ifeq12da  4526  cantnflem1d  9656  cantnflem1  9657  dfac12lem1  10126  xrmaxeq  13204  xrmineq  13205  rexmul  13296  max0add  15360  sumeq2ii  15743  fsumser  15780  ramcl  17088  dmdprdsplitlem  20108  coe1pwmul  22408  scmatscmiddistr  22633  mulmarep1gsum1  22698  maducoeval2  22765  madugsum  22768  madurid  22769  ptcld  23738  ibllem  25891  itgvallem3  25913  iblposlem  25919  iblss2  25933  iblmulc2  25958  cnplimc  26014  limcco  26020  dvexp3  26105  dchrinvcl  27382  lgsval2lem  27436  lgsval4lem  27437  lgsneg  27450  lgsmod  27452  lgsdilem2  27462  rpvmasum2  27641  esplyind  33909  mrsubrn  35903  ftc1anclem6  38236  ftc1anclem8  38238  fsuppind  43213