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

Theorem iffalse 3367
 Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
Assertion
Ref Expression
iffalse 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Proof of Theorem iffalse
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dedlemb 912 . . 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:  iffalsei  3368  iffalsed  3369  ifnefalse  3370  ifsbdc  3371  ifcldadc  3386  ifeq1dadc  3387  ifbothdc  3388  ifcldcd  3389  fidifsnen  6405  uzin  8732  modifeq2int  9468  expival  9575  bcval  9773  bcval3  9775  isumrblem  10337  fisumcvg  10338  flodddiv4  10478  gcdn0val  10497  dfgcd2  10547  lcmn0val  10592
 Copyright terms: Public domain W3C validator