Theorem ifeq1da 4514

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 4502	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4491	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4491	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2799	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 487	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 825	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-if 4483

This theorem is used by:  ifeq12da  4516  cantnflem1d  9689  cantnflem1  9690  dfac12lem1  10222  xrmaxeq  13309  xrmineq  13310  rexmul  13401  max0add  15477  sumeq2ii  15860  fsumser  15896  ramcl  17207  dmdprdsplitlem  20253  coe1pwmul  22598  scmatscmiddistr  22823  mulmarep1gsum1  22888  maducoeval2  22955  madugsum  22958  madurid  22959  ptcld  23932  ibllem  26085  itgvallem3  26106  iblposlem  26112  iblss2  26126  iblmulc2  26151  cnplimc  26207  limcco  26213  dvexp3  26298  dchrinvcl  27580  lgsval2lem  27634  lgsval4lem  27635  lgsneg  27648  lgsmod  27650  lgsdilem2  27660  rpvmasum2  27839  esplyind  34207  mrsubrn  36278  ftc1anclem6  38616  ftc1anclem8  38618  fsuppind  43618