Theorem negsym1 32416

Description: In the paper "On Variable Functors of Propositional Arguments", Lukasiewicz introduced a system that can handle variable connectives. This was done by introducing a variable, marked with a lowercase delta, which takes a wff as input. In the system, "delta ph " means that "something is true of ph." "delta ph " can be substituted with -. ph, ps /\ ph, A. x ph, etc.

Later on, Meredith discovered a single axiom, in the form of ( delta delta F. -> delta ph ). This represents the shortest theorem in the extended propositional calculus that cannot be derived as an instance of a theorem in propositional calculus.

A symmetry with -.. (Contributed by Anthony Hart, 4-Sep-2011.)

Assertion

Ref	Expression
negsym1	|- ( -. -. F. -> -. ph )

Proof of Theorem negsym1

Step	Hyp	Ref	Expression
1		fal 1490	. 2 |- -. F.
2	1	pm2.24i 146	1 |- ( -. -. F. -> -. ph )

Syntax hints:   -. wn 3   -> wi 4   F. wfal 1488

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 197  df-tru 1486  df-fal 1489

This theorem is referenced by: (None)