Theorem un0.1 45760

Description: ⊤ is the constant true, a tautology (see df-tru 1573). 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 45553	. . 3 ⊢ (⊤ → 𝜑)
3		un0.1.2	. . . 4 ⊢ (   𝜓   ▶   𝜒   )
4	3	in1 45553	. . 3 ⊢ (𝜓 → 𝜒)
5		un0.1.3	. . . 4 ⊢ (   (   ⊤   ,   𝜓   )   ▶   𝜃   )
6	5	dfvd2ani 45565	. . 3 ⊢ ((⊤ ∧ 𝜓) → 𝜃)
7	2, 4, 6	uun0.1 45759	. 2 ⊢ (𝜓 → 𝜃)
8	7	dfvd1ir 45555	1 ⊢ (   𝜓   ▶   𝜃   )

This proof depends on syntax axioms:  ⊤wtru 1571  (   wvd1 45551  (   wvhc2 45562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-vd1 45552  df-vhc2 45563

This theorem is used by:  sspwimpVD  45900