| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > merco1 | Structured version Visualization version GIF version | ||
| Description: A single axiom for
propositional calculus discovered by C. A. Meredith.
This axiom is worthy of note, due to it having only 19 symbols, not counting parentheses. The more well-known meredith 1661 has 21 symbols, sans parentheses. See merco2 1756 for another axiom of equal length. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| merco1 | ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-1 6 | . . . . . 6 ⊢ (¬ 𝜒 → (¬ 𝜃 → ¬ 𝜒)) | |
| 2 | falim 1577 | . . . . . 6 ⊢ (⊥ → (¬ 𝜃 → ¬ 𝜒)) | |
| 3 | 1, 2 | ja 187 | . . . . 5 ⊢ ((𝜒 → ⊥) → (¬ 𝜃 → ¬ 𝜒)) |
| 4 | 3 | imim2i 16 | . . . 4 ⊢ (((𝜑 → 𝜓) → (𝜒 → ⊥)) → ((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒))) |
| 5 | 4 | imim1i 63 | . . 3 ⊢ ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → (((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃)) |
| 6 | 5 | imim1i 63 | . 2 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏)) |
| 7 | meredith 1661 | . 2 ⊢ (((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑))) | |
| 8 | 6, 7 | syl 17 | 1 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑))) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ⊥wfal 1572 |
| 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 209 df-tru 1563 df-fal 1573 |
| This theorem is referenced by: merco1lem1 1734 retbwax2 1736 merco1lem2 1737 merco1lem4 1739 merco1lem5 1740 merco1lem6 1741 merco1lem7 1742 merco1lem10 1746 merco1lem11 1747 merco1lem12 1748 merco1lem13 1749 merco1lem14 1750 merco1lem16 1752 merco1lem17 1753 merco1lem18 1754 retbwax1 1755 |
| Copyright terms: Public domain | W3C validator |