Theorem ifeq1da 4487

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 4475	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4465	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4465	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2781	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 481	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 809	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-if 4457

This theorem is referenced by:  ifeq12da  4489  cantnflem1d  9376  cantnflem1  9377  dfac12lem1  9830  xrmaxeq  12842  xrmineq  12843  rexmul  12934  max0add  14950  sumeq2ii  15333  fsumser  15370  ramcl  16658  dmdprdsplitlem  19555  coe1pwmul  21360  scmatscmiddistr  21565  mulmarep1gsum1  21630  maducoeval2  21697  madugsum  21700  madurid  21701  ptcld  22672  ibllem  24834  itgvallem3  24855  iblposlem  24861  iblss2  24875  iblmulc2  24900  cnplimc  24956  limcco  24962  dvexp3  25047  dchrinvcl  26306  lgsval2lem  26360  lgsval4lem  26361  lgsneg  26374  lgsmod  26376  lgsdilem2  26386  rpvmasum2  26565  mrsubrn  33375  ftc1anclem6  35782  ftc1anclem8  35784  fsuppind  40202