Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  un0.1 Structured version   Visualization version   GIF version

Theorem un0.1 41472
 Description: ⊤ is the constant true, a tautology (see df-tru 1541). Kleene's "empty conjunction" is logically equivalent to ⊤. In a virtual deduction we shall interpret ⊤ to be the empty wff or the empty collection of virtual hypotheses. ⊤ in a virtual deduction translated into conventional notation we shall interpret to be Kleene's empty conjunction. If 𝜃 is true given the empty collection of virtual hypotheses and another collection of virtual hypotheses, then it is true given only the other collection of virtual hypotheses. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
un0.1.1 (      ▶   𝜑   )
un0.1.2 (   𝜓   ▶   𝜒   )
un0.1.3 (   (      ,   𝜓   )   ▶   𝜃   )
Assertion
Ref Expression
un0.1 (   𝜓   ▶   𝜃   )

Proof of Theorem un0.1
StepHypRef Expression
1 un0.1.1 . . . 4 (      ▶   𝜑   )
21in1 41264 . . 3 (⊤ → 𝜑)
3 un0.1.2 . . . 4 (   𝜓   ▶   𝜒   )
43in1 41264 . . 3 (𝜓𝜒)
5 un0.1.3 . . . 4 (   (      ,   𝜓   )   ▶   𝜃   )
65dfvd2ani 41276 . . 3 ((⊤ ∧ 𝜓) → 𝜃)
72, 4, 6uun0.1 41471 . 2 (𝜓𝜃)
87dfvd1ir 41266 1 (   𝜓   ▶   𝜃   )
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1539  (   wvd1 41262  (   wvhc2 41273 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-vd1 41263  df-vhc2 41274 This theorem is referenced by:  sspwimpVD  41612
 Copyright terms: Public domain W3C validator