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(𝜑, 𝐴, 𝐵) = 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 720   = wceq 1402   ∈ wcel 2209  {cab 2224  ifcif 3638

This proof depends on 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 proof 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 used 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  7139  fidifsnen  7177  nnnninf  7473  nnnninf2  7474  mkvprop  7505  iftrueb01  7589  ind1  9310  uzin  9972  fzprval  10507  fztpval  10508  modifeq2int  10845  seqf1oglem1  10978  seqf1oglem2  10979  bcval  11210  bcval2  11211  ccatval1  11388  ccatalpha  11404  swrdccat  11530  pfxccat3a  11533  swrdccat3b  11535  sumrbdclem  12170  fsum3cvg  12171  summodclem2a  12174  isumss2  12186  fsum3ser  12190  fsumsplit  12200  sumsplitdc  12225  prodrbdclem  12364  fproddccvg  12365  iprodap  12373  iprodap0  12375  prodssdc  12382  fprodsplitdc  12389  flodddiv4  12729  gcd0val  12763  dfgcd2  12817  eucalgf  12859  eucalginv  12860  eucalglt  12861  phisum  13049  pc0  13113  pcgcd  13138  pcmptcl  13151  pcmpt  13152  pcmpt2  13153  pcprod  13155  fldivp1  13157  1arithlem4  13175  ballotfilemsima  13318  ballotfilemrv1  13323  unct  13392  xpsfrnel  13725  znf1o  15096  psrlidmfi  15204  psrridmfi  15205  mvrf1fi  15215  dvexp2  15950  elply2  15973  elplyd  15979  ply1termlem  15980  chtublem  16307  bposlem1  16323  bposlem3  16325  bposlem5  16327  bposlem6  16328  lgsval2lem  16346  lgsneg  16360  lgsdilem  16363  lgsdir2  16369  lgsdir  16371  lgsdi  16373  lgsne0  16374  gausslemma2dlem1a  16394  2lgslem1c  16426  2lgslem3  16437  2lgs  16440  opvtxval  16479  opiedgval  16482  depindlem1  16964  nnsf  17266  nninfsellemsuc  17273