Theorem negsym1 36418

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 𝜑 " means that "something is true of 𝜑". The expression "delta 𝜑 " can be substituted with ¬ 𝜑, 𝜓 ∧ 𝜑, ∀𝑥𝜑, etc.

Later on, Meredith discovered a single axiom, in the form of ( delta delta ⊥ → delta 𝜑 ). 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	⊢ (¬ ¬ ⊥ → ¬ 𝜑)

Proof of Theorem negsym1

Step	Hyp	Ref	Expression
1		fal 1554	. 2 ⊢ ¬ ⊥
2	1	pm2.24i 150	1 ⊢ (¬ ¬ ⊥ → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ⊥wfal 1552

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 207  df-tru 1543  df-fal 1553

This theorem is referenced by: (None)