ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  iftrue GIF version

Theorem iftrue 3523
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.
StepHypRef Expression
1 df-if 3519 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
2 dedlema 958 . . 3 (𝜑 → (𝑥𝐴 ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))))
32abbi2dv 2283 . 2 (𝜑𝐴 = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))})
41, 3eqtr4id 2216 1 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 698   = wceq 1342  wcel 2135  {cab 2150  ifcif 3518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-if 3519
This theorem is referenced by:  iftruei  3524  iftrued  3525  ifsbdc  3530  ifcldadc  3547  ifbothdadc  3549  ifbothdc  3550  ifiddc  3551  ifcldcd  3553  ifandc  3554  fidifsnen  6830  nnnninf  7084  nnnninf2  7085  mkvprop  7116  uzin  9492  fzprval  10011  fztpval  10012  modifeq2int  10315  bcval  10656  bcval2  10657  sumrbdclem  11312  fsum3cvg  11313  summodclem2a  11316  isumss2  11328  fsum3ser  11332  fsumsplit  11342  sumsplitdc  11367  prodrbdclem  11506  fproddccvg  11507  iprodap  11515  iprodap0  11517  prodssdc  11524  fprodsplitdc  11531  flodddiv4  11865  gcd0val  11887  dfgcd2  11941  eucalgf  11981  eucalginv  11982  eucalglt  11983  phisum  12166  pc0  12230  pcgcd  12254  pcmptcl  12266  pcmpt  12267  pcmpt2  12268  pcprod  12270  fldivp1  12272  1arithlem4  12290  unct  12369  dvexp2  13274  nnsf  13778  nninfsellemsuc  13785
  Copyright terms: Public domain W3C validator