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

Theorem merco1 1785
 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.)
Assertion
Ref Expression
merco1 (((((𝜑𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏𝜑) → (𝜒𝜑)))

Proof of Theorem merco1
StepHypRef Expression
1 ax-1 6 . . . . . 6 𝜒 → (¬ 𝜃 → ¬ 𝜒))
2 falim 1645 . . . . . 6 (⊥ → (¬ 𝜃 → ¬ 𝜒))
31, 2ja 174 . . . . 5 ((𝜒 → ⊥) → (¬ 𝜃 → ¬ 𝜒))
43imim2i 16 . . . 4 (((𝜑𝜓) → (𝜒 → ⊥)) → ((𝜑𝜓) → (¬ 𝜃 → ¬ 𝜒)))
54imim1i 63 . . 3 ((((𝜑𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → (((𝜑𝜓) → (𝜒 → ⊥)) → 𝜃))
65imim1i 63 . 2 (((((𝜑𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((((𝜑𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏))
7 meredith 1713 . 2 (((((𝜑𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏) → ((𝜏𝜑) → (𝜒𝜑)))
86, 7syl 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