Theorem ifeq1da 4093

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1480  ifcif 4063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rab 2921  df-v 3193  df-un 3565  df-if 4064

This theorem is referenced by:  ifeq12da  4095  cantnflem1d  8530  cantnflem1  8531  dfac12lem1  8910  xrmaxeq  11952  xrmineq  11953  rexmul  12041  max0add  13979  sumeq2ii  14352  fsumser  14389  ramcl  15652  dmdprdsplitlem  18352  coe1pwmul  19563  scmatscmiddistr  20228  mulmarep1gsum1  20293  maducoeval2  20360  madugsum  20363  madurid  20364  ptcld  21321  copco  22721  ibllem  23432  itgvallem3  23453  iblposlem  23459  iblss2  23473  iblmulc2  23498  cnplimc  23552  limcco  23558  dvexp3  23640  dchrinvcl  24873  lgsval2lem  24927  lgsval4lem  24928  lgsneg  24941  lgsmod  24943  lgsdilem2  24953  rpvmasum2  25096  mrsubrn  31110  ftc1anclem6  33108  ftc1anclem8  33110