Theorem ifeq1da 4513

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 4501	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4490	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4490	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2798	. . 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 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 4151  df-if 4482

This theorem is used by:  ifeq12da  4515  cantnflem1d  9690  cantnflem1  9691  dfac12lem1  10223  xrmaxeq  13310  xrmineq  13311  rexmul  13402  max0add  15478  sumeq2ii  15861  fsumser  15897  ramcl  17208  dmdprdsplitlem  20254  coe1pwmul  22599  scmatscmiddistr  22824  mulmarep1gsum1  22889  maducoeval2  22956  madugsum  22959  madurid  22960  ptcld  23933  ibllem  26086  itgvallem3  26107  iblposlem  26113  iblss2  26127  iblmulc2  26152  cnplimc  26208  limcco  26214  dvexp3  26299  dchrinvcl  27581  lgsval2lem  27635  lgsval4lem  27636  lgsneg  27649  lgsmod  27651  lgsdilem2  27661  rpvmasum2  27840  esplyind  34250  mrsubrn  36347  ftc1anclem6  38692  ftc1anclem8  38694  fsuppind  43694