Theorem iftrue 3607

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 713   = wceq 1395   ∈ wcel 2200  {cab 2215  ifcif 3602

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  iftruei  3608  iftrued  3609  ifsbdc  3615  ifcldadc  3632  ifeqdadc  3635  ifbothdadc  3636  ifbothdc  3637  ifiddc  3638  ifcldcd  3640  ifnotdc  3641  2if2dc  3642  ifandc  3643  ifordc  3644  ifnefals  3647  pw2f1odclem  7008  fidifsnen  7045  nnnninf  7309  nnnninf2  7310  mkvprop  7341  iftrueb01  7424  uzin  9772  fzprval  10295  fztpval  10296  modifeq2int  10625  seqf1oglem1  10758  seqf1oglem2  10759  bcval  10988  bcval2  10989  ccatval1  11150  ccatalpha  11166  swrdccat  11288  pfxccat3a  11291  swrdccat3b  11293  sumrbdclem  11909  fsum3cvg  11910  summodclem2a  11913  isumss2  11925  fsum3ser  11929  fsumsplit  11939  sumsplitdc  11964  prodrbdclem  12103  fproddccvg  12104  iprodap  12112  iprodap0  12114  prodssdc  12121  fprodsplitdc  12128  flodddiv4  12468  gcd0val  12502  dfgcd2  12556  eucalgf  12598  eucalginv  12599  eucalglt  12600  phisum  12784  pc0  12848  pcgcd  12873  pcmptcl  12886  pcmpt  12887  pcmpt2  12888  pcprod  12890  fldivp1  12892  1arithlem4  12910  unct  13034  xpsfrnel  13398  znf1o  14636  dvexp2  15407  elply2  15430  elplyd  15436  ply1termlem  15437  lgsval2lem  15710  lgsneg  15724  lgsdilem  15727  lgsdir2  15733  lgsdir  15735  lgsdi  15737  lgsne0  15738  gausslemma2dlem1a  15758  2lgslem1c  15790  2lgslem3  15801  2lgs  15804  opvtxval  15843  opiedgval  15846  nnsf  16485  nninfsellemsuc  16492