MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  merco1 Structured version   Visualization version   GIF version

Theorem merco1 1812
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 1740 has 21 symbols, sans parentheses.

See merco2 1835 for another axiom of equal length. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion
Ref Expression
merco1 (((((𝜑𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏𝜑) → (𝜒𝜑)))

Proof of Theorem merco1
StepHypRef Expression
1 ax-1 6 . . . . . 6 𝜒 → (¬ 𝜃 → ¬ 𝜒))
2 falim 1674 . . . . . 6 (⊥ → (¬ 𝜃 → ¬ 𝜒))
31, 2ja 175 . . . . 5 ((𝜒 → ⊥) → (¬ 𝜃 → ¬ 𝜒))
43imim2i 16 . . . 4 (((𝜑𝜓) → (𝜒 → ⊥)) → ((𝜑𝜓) → (¬ 𝜃 → ¬ 𝜒)))
54imim1i 63 . . 3 ((((𝜑𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → (((𝜑𝜓) → (𝜒 → ⊥)) → 𝜃))
65imim1i 63 . 2 (((((𝜑𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((((𝜑𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏))
7 meredith 1740 . 2 (((((𝜑𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏) → ((𝜏𝜑) → (𝜒𝜑)))
86, 7syl 17 1 (((((𝜑𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏𝜑) → (𝜒𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wfal 1669
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 199  df-tru 1660  df-fal 1670
This theorem is referenced by:  merco1lem1  1813  retbwax2  1815  merco1lem2  1816  merco1lem4  1818  merco1lem5  1819  merco1lem6  1820  merco1lem7  1821  merco1lem10  1825  merco1lem11  1826  merco1lem12  1827  merco1lem13  1828  merco1lem14  1829  merco1lem16  1831  merco1lem17  1832  merco1lem18  1833  retbwax1  1834
  Copyright terms: Public domain W3C validator