Theorem ifeq1da 4451

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 4439	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4429	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4429	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2796	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 485	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 812	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538  ifcif 4420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-un 3863  df-if 4421

This theorem is referenced by:  ifeq12da  4453  cantnflem1d  9184  cantnflem1  9185  dfac12lem1  9603  xrmaxeq  12613  xrmineq  12614  rexmul  12705  max0add  14718  sumeq2ii  15098  fsumser  15135  ramcl  16420  dmdprdsplitlem  19227  coe1pwmul  21003  scmatscmiddistr  21208  mulmarep1gsum1  21273  maducoeval2  21340  madugsum  21343  madurid  21344  ptcld  22313  ibllem  24464  itgvallem3  24485  iblposlem  24491  iblss2  24505  iblmulc2  24530  cnplimc  24586  limcco  24592  dvexp3  24677  dchrinvcl  25936  lgsval2lem  25990  lgsval4lem  25991  lgsneg  26004  lgsmod  26006  lgsdilem2  26016  rpvmasum2  26195  mrsubrn  32991  ftc1anclem6  35437  ftc1anclem8  35439  fsuppind  39806