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

Theorem iftrue 3364
 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 dedlema 911 . . 3 (𝜑 → (𝑥𝐴 ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))))
21abbi2dv 2198 . 2 (𝜑𝐴 = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))})
3 df-if 3360 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
42, 3syl6reqr 2133 1 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ∨ wo 662   = wceq 1285   ∈ wcel 1434  {cab 2068  ifcif 3359 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-if 3360 This theorem is referenced by:  iftruei  3365  iftrued  3366  ifsbdc  3371  ifcldadc  3386  ifbothdc  3388  ifcldcd  3389  fidifsnen  6405  uzin  8732  fzprval  9175  fztpval  9176  modifeq2int  9468  expival  9575  bcval  9773  bcval2  9774  isumrblem  10337  fisumcvg  10338  flodddiv4  10478  gcd0val  10496  dfgcd2  10547  eucalgf  10581  eucalginv  10582  eucalglt  10583
 Copyright terms: Public domain W3C validator