Theorem iftrue 3567

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 709   = wceq 1364   ∈ wcel 2167  {cab 2182  ifcif 3562

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-if 3563

This theorem is referenced by:  iftruei  3568  iftrued  3569  ifsbdc  3574  ifcldadc  3591  ifbothdadc  3594  ifbothdc  3595  ifiddc  3596  ifcldcd  3598  ifnotdc  3599  ifandc  3600  ifordc  3601  ifnefals  3604  pw2f1odclem  6904  fidifsnen  6940  nnnninf  7201  nnnninf2  7202  mkvprop  7233  uzin  9651  fzprval  10174  fztpval  10175  modifeq2int  10495  seqf1oglem1  10628  seqf1oglem2  10629  bcval  10858  bcval2  10859  sumrbdclem  11559  fsum3cvg  11560  summodclem2a  11563  isumss2  11575  fsum3ser  11579  fsumsplit  11589  sumsplitdc  11614  prodrbdclem  11753  fproddccvg  11754  iprodap  11762  iprodap0  11764  prodssdc  11771  fprodsplitdc  11778  flodddiv4  12118  gcd0val  12152  dfgcd2  12206  eucalgf  12248  eucalginv  12249  eucalglt  12250  phisum  12434  pc0  12498  pcgcd  12523  pcmptcl  12536  pcmpt  12537  pcmpt2  12538  pcprod  12540  fldivp1  12542  1arithlem4  12560  unct  12684  xpsfrnel  13046  znf1o  14283  dvexp2  15032  elply2  15055  elplyd  15061  ply1termlem  15062  lgsval2lem  15335  lgsneg  15349  lgsdilem  15352  lgsdir2  15358  lgsdir  15360  lgsdi  15362  lgsne0  15363  gausslemma2dlem1a  15383  2lgslem1c  15415  2lgslem3  15426  2lgs  15429  nnsf  15736  nninfsellemsuc  15743