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  7134  fidifsnen  7172  nnnninf  7466  nnnninf2  7467  mkvprop  7498  iftrueb01  7582  ind1  9301  uzin  9957  fzprval  10491  fztpval  10492  modifeq2int  10825  seqf1oglem1  10958  seqf1oglem2  10959  bcval  11189  bcval2  11190  ccatval1  11367  ccatalpha  11383  swrdccat  11509  pfxccat3a  11512  swrdccat3b  11514  sumrbdclem  12146  fsum3cvg  12147  summodclem2a  12150  isumss2  12162  fsum3ser  12166  fsumsplit  12176  sumsplitdc  12201  prodrbdclem  12340  fproddccvg  12341  iprodap  12349  iprodap0  12351  prodssdc  12358  fprodsplitdc  12365  flodddiv4  12705  gcd0val  12739  dfgcd2  12793  eucalgf  12835  eucalginv  12836  eucalglt  12837  phisum  13021  pc0  13085  pcgcd  13110  pcmptcl  13123  pcmpt  13124  pcmpt2  13125  pcprod  13127  fldivp1  13129  1arithlem4  13147  ballotfilemsima  13261  ballotfilemrv1  13266  unct  13335  xpsfrnel  13667  znf1o  14988  dvexp2  15815  elply2  15838  elplyd  15844  ply1termlem  15845  lgsval2lem  16141  lgsneg  16155  lgsdilem  16158  lgsdir2  16164  lgsdir  16166  lgsdi  16168  lgsne0  16169  gausslemma2dlem1a  16189  2lgslem1c  16221  2lgslem3  16232  2lgs  16235  opvtxval  16274  opiedgval  16277  depindlem1  16759  nnsf  17060  nninfsellemsuc  17067