![]() |
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 offered by Meredith.
This axiom is worthy of note, due to it having only 19 symbols, not counting parentheses. The more well-known meredith 1713 has 21 symbols, sans parentheses. See merco2 1808 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 1645 | . . . . . 6 ⊢ (⊥ → (¬ 𝜃 → ¬ 𝜒)) | |
3 | 1, 2 | ja 174 | . . . . 5 ⊢ ((𝜒 → ⊥) → (¬ 𝜃 → ¬ 𝜒)) |
4 | 3 | imim2i 16 | . . . 4 ⊢ (((𝜑 → 𝜓) → (𝜒 → ⊥)) → ((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒))) |
5 | 4 | imim1i 63 | . . 3 ⊢ ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → (((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃)) |
6 | 5 | imim1i 63 | . 2 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏)) |
7 | meredith 1713 | . 2 ⊢ (((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑))) | |
8 | 6, 7 | syl 17 | 1 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ⊥wfal 1635 |
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 197 df-tru 1633 df-fal 1636 |
This theorem is referenced by: merco1lem1 1786 retbwax2 1788 merco1lem2 1789 merco1lem4 1791 merco1lem5 1792 merco1lem6 1793 merco1lem7 1794 merco1lem10 1798 merco1lem11 1799 merco1lem12 1800 merco1lem13 1801 merco1lem14 1802 merco1lem16 1804 merco1lem17 1805 merco1lem18 1806 retbwax1 1807 |
Copyright terms: Public domain | W3C validator |