Theorem ifeq1da 4261

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 4249	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4240	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4240	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2798	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 473	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 867	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1632  ifcif 4231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rab 3060  df-v 3343  df-un 3721  df-if 4232

This theorem is referenced by:  ifeq12da  4263  cantnflem1d  8761  cantnflem1  8762  dfac12lem1  9178  xrmaxeq  12224  xrmineq  12225  rexmul  12315  max0add  14270  sumeq2ii  14643  fsumser  14681  ramcl  15956  dmdprdsplitlem  18657  coe1pwmul  19872  scmatscmiddistr  20537  mulmarep1gsum1  20602  maducoeval2  20669  madugsum  20672  madurid  20673  ptcld  21639  copco  23039  ibllem  23751  itgvallem3  23772  iblposlem  23778  iblss2  23792  iblmulc2  23817  cnplimc  23871  limcco  23877  dvexp3  23961  dchrinvcl  25199  lgsval2lem  25253  lgsval4lem  25254  lgsneg  25267  lgsmod  25269  lgsdilem2  25279  rpvmasum2  25422  mrsubrn  31739  ftc1anclem6  33822  ftc1anclem8  33824