Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-luk2 | Structured version Visualization version GIF version |
Description: 2 of 3 axioms for
propositional calculus due to Lukasiewicz. Copy of
luk-2 1658 or pm2.18 128, but introduced as an axiom. The core idea
behind
this axiom is, that if something can be implied from both an antecedent,
and separately from its negation, then the antecedent is irrelevant to the
consequent, and can safely be dropped. This is perhaps better seen from
the following slightly extended version (related to pm2.65 196):
((𝜑 → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑)). (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-luk2 | ⊢ ((¬ 𝜑 → 𝜑) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | 1 | wn 3 | . 2 wff ¬ 𝜑 |
3 | 2, 1, 1 | bj-0 34271 | 1 wff ((¬ 𝜑 → 𝜑) → 𝜑) |
Colors of variables: wff setvar class |
This axiom is referenced by: wl-luk-pm2.18d 35123 wl-luk-ax3 35130 wl-luk-pm2.27 35132 wl-luk-id 35140 |
Copyright terms: Public domain | W3C validator |