Theorem un0.1

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

	Ref	Expression
Hypotheses	un0.1.1	|- (. T. ->. ph ).
	un0.1.2	|- (. ps ->. ch ).
	un0.1.3	|- (. (. T. ,. ps ). ->. th ).
Assertion	un0.1	|- (. ps ->. th ).

Proof

Step	Hyp	Ref	Expression
1		un0.1.1	|- (. T. ->. ph ).
2		un0.1.2	|- (. ps ->. ch ).
3		un0.1.3	|- (. (. T. ,. ps ). ->. th ).
4	1	in1	|- ( T. -> ph )
5	2	in1	|- ( ps -> ch )
6	3	dfvd2ani	|- ( ( T. /\ ps ) -> th )
7	4 5 6	uun0.1	|- ( ps -> th )
8	7	dfvd1ir	|- (. ps ->. th ).