Theorem ifeq1da 4519

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 4507	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4496	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4496	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2801	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 486	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 824	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1570  ifcif 4487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3910  df-if 4488

This theorem is referenced by:  ifeq12da  4521  cantnflem1d  9653  cantnflem1  9654  dfac12lem1  10123  xrmaxeq  13200  xrmineq  13201  rexmul  13292  max0add  15357  sumeq2ii  15740  fsumser  15777  ramcl  17084  dmdprdsplitlem  20104  coe1pwmul  22440  scmatscmiddistr  22665  mulmarep1gsum1  22730  maducoeval2  22797  madugsum  22800  madurid  22801  ptcld  23770  ibllem  25923  itgvallem3  25945  iblposlem  25951  iblss2  25965  iblmulc2  25990  cnplimc  26046  limcco  26052  dvexp3  26137  dchrinvcl  27417  lgsval2lem  27471  lgsval4lem  27472  lgsneg  27485  lgsmod  27487  lgsdilem2  27497  rpvmasum2  27676  esplyind  33965  mrsubrn  36005  ftc1anclem6  38349  ftc1anclem8  38351  fsuppind  43322