Theorem un0.1 44362

Description: ⊤ is the constant true, a tautology (see df-tru 1536). 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

Step	Hyp	Ref	Expression
1		un0.1.1	. . . 4 ⊢ (   ⊤   ▶   𝜑   )
2	1	in1 44154	. . 3 ⊢ (⊤ → 𝜑)
3		un0.1.2	. . . 4 ⊢ (   𝜓   ▶   𝜒   )
4	3	in1 44154	. . 3 ⊢ (𝜓 → 𝜒)
5		un0.1.3	. . . 4 ⊢ (   (   ⊤   ,   𝜓   )   ▶   𝜃   )
6	5	dfvd2ani 44166	. . 3 ⊢ ((⊤ ∧ 𝜓) → 𝜃)
7	2, 4, 6	uun0.1 44361	. 2 ⊢ (𝜓 → 𝜃)
8	7	dfvd1ir 44156	1 ⊢ (   𝜓   ▶   𝜃   )

Syntax hints:  ⊤wtru 1534  (   wvd1 44152  (   wvhc2 44163

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 206  df-an 395  df-tru 1536  df-vd1 44153  df-vhc2 44164

This theorem is referenced by:  sspwimpVD  44502