Theorem ifeq1da 4307

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 4295	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4286	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4286	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2836	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 474	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 848	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 385   = wceq 1653  ifcif 4277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-un 3774  df-if 4278

This theorem is referenced by:  ifeq12da  4309  cantnflem1d  8835  cantnflem1  8836  dfac12lem1  9253  xrmaxeq  12259  xrmineq  12260  rexmul  12350  max0add  14391  sumeq2ii  14764  fsumser  14802  ramcl  16066  dmdprdsplitlem  18752  coe1pwmul  19971  scmatscmiddistr  20640  mulmarep1gsum1  20705  maducoeval2  20772  madugsum  20775  madurid  20776  ptcld  21745  copco  23145  ibllem  23872  itgvallem3  23893  iblposlem  23899  iblss2  23913  iblmulc2  23938  cnplimc  23992  limcco  23998  dvexp3  24082  dchrinvcl  25330  lgsval2lem  25384  lgsval4lem  25385  lgsneg  25398  lgsmod  25400  lgsdilem2  25410  rpvmasum2  25553  mrsubrn  31927  ftc1anclem6  33978  ftc1anclem8  33980