Theorem iftrue 3645

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 720   = wceq 1402   ∈ wcel 2209  {cab 2224  ifcif 3638

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 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is referenced by:  iftruei  3646  iftrued  3647  ifsbdc  3653  ifcldadc  3670  ifeqdadc  3673  ifbothdadc  3674  ifbothdc  3675  ifiddc  3676  ifcldcd  3678  ifnotdc  3679  2if2dc  3680  ifandc  3681  ifordc  3682  ifnefals  3685  pw2f1odclem  7128  fidifsnen  7166  nnnninf  7460  nnnninf2  7461  mkvprop  7492  iftrueb01  7576  uzin  9938  fzprval  10472  fztpval  10473  modifeq2int  10806  seqf1oglem1  10939  seqf1oglem2  10940  bcval  11170  bcval2  11171  ccatval1  11348  ccatalpha  11364  swrdccat  11490  pfxccat3a  11493  swrdccat3b  11495  sumrbdclem  12127  fsum3cvg  12128  summodclem2a  12131  isumss2  12143  fsum3ser  12147  fsumsplit  12157  sumsplitdc  12182  prodrbdclem  12321  fproddccvg  12322  iprodap  12330  iprodap0  12332  prodssdc  12339  fprodsplitdc  12346  flodddiv4  12686  gcd0val  12720  dfgcd2  12774  eucalgf  12816  eucalginv  12817  eucalglt  12818  phisum  13002  pc0  13066  pcgcd  13091  pcmptcl  13104  pcmpt  13105  pcmpt2  13106  pcprod  13108  fldivp1  13110  1arithlem4  13128  ballotfilemsima  13242  ballotfilemrv1  13247  unct  13316  xpsfrnel  13648  znf1o  14969  dvexp2  15796  elply2  15819  elplyd  15825  ply1termlem  15826  lgsval2lem  16112  lgsneg  16126  lgsdilem  16129  lgsdir2  16135  lgsdir  16137  lgsdi  16139  lgsne0  16140  gausslemma2dlem1a  16160  2lgslem1c  16192  2lgslem3  16203  2lgs  16206  opvtxval  16245  opiedgval  16248  depindlem1  16730  nnsf  17022  nninfsellemsuc  17029