Theorem iftrue 3562

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		df-if 3558	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlema 971	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
3	2	abbi2dv 2312	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
4	1, 3	eqtr4id 2245	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 709   = wceq 1364   ∈ wcel 2164  {cab 2179  ifcif 3557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-if 3558

This theorem is referenced by:  iftruei  3563  iftrued  3564  ifsbdc  3569  ifcldadc  3586  ifbothdadc  3589  ifbothdc  3590  ifiddc  3591  ifcldcd  3593  ifnotdc  3594  ifandc  3595  ifordc  3596  ifnefals  3599  pw2f1odclem  6890  fidifsnen  6926  nnnninf  7185  nnnninf2  7186  mkvprop  7217  uzin  9625  fzprval  10148  fztpval  10149  modifeq2int  10457  seqf1oglem1  10590  seqf1oglem2  10591  bcval  10820  bcval2  10821  sumrbdclem  11520  fsum3cvg  11521  summodclem2a  11524  isumss2  11536  fsum3ser  11540  fsumsplit  11550  sumsplitdc  11575  prodrbdclem  11714  fproddccvg  11715  iprodap  11723  iprodap0  11725  prodssdc  11732  fprodsplitdc  11739  flodddiv4  12075  gcd0val  12097  dfgcd2  12151  eucalgf  12193  eucalginv  12194  eucalglt  12195  phisum  12378  pc0  12442  pcgcd  12467  pcmptcl  12480  pcmpt  12481  pcmpt2  12482  pcprod  12484  fldivp1  12486  1arithlem4  12504  unct  12599  xpsfrnel  12927  znf1o  14139  dvexp2  14861  elply2  14881  elplyd  14887  ply1termlem  14888  lgsval2lem  15126  lgsneg  15140  lgsdilem  15143  lgsdir2  15149  lgsdir  15151  lgsdi  15153  lgsne0  15154  gausslemma2dlem1a  15174  nnsf  15495  nninfsellemsuc  15502