Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  un0.1 Unicode version

Theorem un0.1 28554
Description:  T. is the constant true, a tautology ( see: df-tru 1310). Kleene's "empty conjunction" is logically equivalent to  T.. In a virtual deduction we shall interpret 
T. to be the empty wff or the empty collection of virtual hypotheses.  T. in a virtual deduction translated into conventional notation we shall interpret to be Kleene's empty conjunction. If  th 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  |-  (.  T.  ->.  ph ).
un0.1.2  |-  (. ps  ->.  ch
).
un0.1.3  |-  (. (.  T.  ,. ps ).  ->.  th ).
Assertion
Ref Expression
un0.1  |-  (. ps  ->.  th
).

Proof of Theorem un0.1
StepHypRef Expression
1 un0.1.1 . . . 4  |-  (.  T.  ->.  ph ).
21in1 28339 . . 3  |-  (  T. 
->  ph )
3 un0.1.2 . . . 4  |-  (. ps  ->.  ch
).
43in1 28339 . . 3  |-  ( ps 
->  ch )
5 un0.1.3 . . . 4  |-  (. (.  T.  ,. ps ).  ->.  th ).
65dfvd2ani 28352 . . 3  |-  ( (  T.  /\  ps )  ->  th )
72, 4, 6uun0.1 28553 . 2  |-  ( ps 
->  th )
87dfvd1ir 28341 1  |-  (. ps  ->.  th
).
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   (.wvd1 28337   (.wvhc2 28349
This theorem is referenced by:  sspwimpVD  28695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-vd1 28338  df-vhc2 28350
  Copyright terms: Public domain W3C validator