Description: From a wff and its negation, anything follows. Theorem *2.21 of WhiteheadRussell p. 104. Also called the Duns Scotus law. Copy of pm2.21 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-luk-pm2.21 | ⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-luk3 | ⊢ ( 𝜑 → ( ¬ 𝜑 → 𝜓 ) ) | |
| 2 | 1 | wl-luk-com12 | ⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) ) |