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 1642 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 194):
((𝜑 → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑)). (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 33492 | 1 wff ((¬ 𝜑 → 𝜑) → 𝜑) |
Colors of variables: wff setvar class |
This axiom is referenced by: wl-luk-pm2.18d 34259 wl-luk-ax3 34266 wl-luk-pm2.27 34268 wl-luk-id 34276 |
Copyright terms: Public domain | W3C validator |