Theorem ifeq1da 4522

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1541  ifcif 4491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-un 3918  df-if 4492

This theorem is referenced by:  ifeq12da  4524  cantnflem1d  9633  cantnflem1  9634  dfac12lem1  10088  xrmaxeq  13108  xrmineq  13109  rexmul  13200  max0add  15207  sumeq2ii  15589  fsumser  15626  ramcl  16912  dmdprdsplitlem  19830  coe1pwmul  21687  scmatscmiddistr  21894  mulmarep1gsum1  21959  maducoeval2  22026  madugsum  22029  madurid  22030  ptcld  23001  ibllem  25166  itgvallem3  25187  iblposlem  25193  iblss2  25207  iblmulc2  25232  cnplimc  25288  limcco  25294  dvexp3  25379  dchrinvcl  26638  lgsval2lem  26692  lgsval4lem  26693  lgsneg  26706  lgsmod  26708  lgsdilem2  26718  rpvmasum2  26897  mrsubrn  34194  ftc1anclem6  36229  ftc1anclem8  36231  fsuppind  40823