|   | 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 1641 has 21 symbols, sans parentheses. See merco2 1736 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 1557 | . . . . . 6 ⊢ (⊥ → (¬ 𝜃 → ¬ 𝜒)) | |
| 3 | 1, 2 | ja 186 | . . . . 5 ⊢ ((𝜒 → ⊥) → (¬ 𝜃 → ¬ 𝜒)) | 
| 4 | 3 | imim2i 16 | . . . 4 ⊢ (((𝜑 → 𝜓) → (𝜒 → ⊥)) → ((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒))) | 
| 5 | 4 | imim1i 63 | . . 3 ⊢ ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → (((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃)) | 
| 6 | 5 | imim1i 63 | . 2 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏)) | 
| 7 | meredith 1641 | . 2 ⊢ (((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑))) | |
| 8 | 6, 7 | syl 17 | 1 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ⊥wfal 1552 | 
| 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 207 df-tru 1543 df-fal 1553 | 
| This theorem is referenced by: merco1lem1 1714 retbwax2 1716 merco1lem2 1717 merco1lem4 1719 merco1lem5 1720 merco1lem6 1721 merco1lem7 1722 merco1lem10 1726 merco1lem11 1727 merco1lem12 1728 merco1lem13 1729 merco1lem14 1730 merco1lem16 1732 merco1lem17 1733 merco1lem18 1734 retbwax1 1735 | 
| Copyright terms: Public domain | W3C validator |