Theorem iftrue 3587

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 712   = wceq 1375   ∈ wcel 2180  {cab 2195  ifcif 3582

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 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-if 3583

This theorem is referenced by:  iftruei  3588  iftrued  3589  ifsbdc  3595  ifcldadc  3612  ifeqdadc  3615  ifbothdadc  3616  ifbothdc  3617  ifiddc  3618  ifcldcd  3620  ifnotdc  3621  2if2dc  3622  ifandc  3623  ifordc  3624  ifnefals  3627  pw2f1odclem  6963  fidifsnen  7000  nnnninf  7261  nnnninf2  7262  mkvprop  7293  iftrueb01  7376  uzin  9723  fzprval  10246  fztpval  10247  modifeq2int  10575  seqf1oglem1  10708  seqf1oglem2  10709  bcval  10938  bcval2  10939  ccatval1  11098  swrdccat  11233  pfxccat3a  11236  swrdccat3b  11238  sumrbdclem  11854  fsum3cvg  11855  summodclem2a  11858  isumss2  11870  fsum3ser  11874  fsumsplit  11884  sumsplitdc  11909  prodrbdclem  12048  fproddccvg  12049  iprodap  12057  iprodap0  12059  prodssdc  12066  fprodsplitdc  12073  flodddiv4  12413  gcd0val  12447  dfgcd2  12501  eucalgf  12543  eucalginv  12544  eucalglt  12545  phisum  12729  pc0  12793  pcgcd  12818  pcmptcl  12831  pcmpt  12832  pcmpt2  12833  pcprod  12835  fldivp1  12837  1arithlem4  12855  unct  12979  xpsfrnel  13343  znf1o  14580  dvexp2  15351  elply2  15374  elplyd  15380  ply1termlem  15381  lgsval2lem  15654  lgsneg  15668  lgsdilem  15671  lgsdir2  15677  lgsdir  15679  lgsdi  15681  lgsne0  15682  gausslemma2dlem1a  15702  2lgslem1c  15734  2lgslem3  15745  2lgs  15748  opvtxval  15787  opiedgval  15790  nnsf  16282  nninfsellemsuc  16289