Theorem iftrue 3426

Description: Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
iftrue	⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Proof of Theorem iftrue

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dedlema 921	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
2	1	abbi2dv 2218	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
3		df-if 3422	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
4	2, 3	syl6reqr 2151	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 670   = wceq 1299   ∈ wcel 1448  {cab 2086  ifcif 3421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-if 3422

This theorem is referenced by:  iftruei  3427  iftrued  3428  ifsbdc  3433  ifcldadc  3448  ifbothdadc  3450  ifbothdc  3451  ifiddc  3452  ifcldcd  3454  ifandc  3455  fidifsnen  6693  nnnninf  6935  mkvprop  6943  uzin  9208  fzprval  9703  fztpval  9704  modifeq2int  10000  bcval  10336  bcval2  10337  sumrbdclem  10984  fsum3cvg  10985  summodclem2a  10989  isumss2  11001  fsum3ser  11005  fsumsplit  11015  sumsplitdc  11040  flodddiv4  11426  gcd0val  11444  dfgcd2  11495  eucalgf  11529  eucalginv  11530  eucalglt  11531  nnsf  12783  nninfsellemsuc  12792