Theorem ifeq1da 4514

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 4502	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		iffalse 4491	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4		iffalse 4491	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
5	3, 4	eqtr4d 2798	. . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
6	5	adantl 487	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
7	2, 6	pm2.61dan 825	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-if 4483

This theorem is used by:  ifeq12da  4516  cantnflem1d  9668  cantnflem1  9669  dfac12lem1  10147  xrmaxeq  13232  xrmineq  13233  rexmul  13324  max0add  15398  sumeq2ii  15781  fsumser  15817  ramcl  17122  dmdprdsplitlem  20167  coe1pwmul  22506  scmatscmiddistr  22731  mulmarep1gsum1  22796  maducoeval2  22863  madugsum  22866  madurid  22867  ptcld  23840  ibllem  25993  itgvallem3  26014  iblposlem  26020  iblss2  26034  iblmulc2  26059  cnplimc  26115  limcco  26121  dvexp3  26206  dchrinvcl  27490  lgsval2lem  27544  lgsval4lem  27545  lgsneg  27558  lgsmod  27560  lgsdilem2  27570  rpvmasum2  27749  esplyind  34086  mrsubrn  36093  ftc1anclem6  38448  ftc1anclem8  38450  fsuppind  43437