Theorem ifeq1da 4512

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1560  ifcif 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-un 3909  df-if 4481

This theorem is referenced by:  ifeq12da  4514  cantnflem1d  9643  cantnflem1  9644  dfac12lem1  10100  xrmaxeq  13182  xrmineq  13183  rexmul  13274  max0add  15337  sumeq2ii  15720  fsumser  15757  ramcl  17065  dmdprdsplitlem  20079  coe1pwmul  22339  scmatscmiddistr  22565  mulmarep1gsum1  22630  maducoeval2  22697  madugsum  22700  madurid  22701  ptcld  23670  ibllem  25823  itgvallem3  25845  iblposlem  25851  iblss2  25865  iblmulc2  25890  cnplimc  25946  limcco  25952  dvexp3  26037  dchrinvcl  27314  lgsval2lem  27368  lgsval4lem  27369  lgsneg  27382  lgsmod  27384  lgsdilem2  27394  rpvmasum2  27573  esplyind  33869  mrsubrn  35860  ftc1anclem6  38194  ftc1anclem8  38196  fsuppind  43169