Theorem merco1 1743

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 1671 has 21 symbols, sans parentheses.

See merco2 1766 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

Step	Hyp	Ref	Expression
1		ax-1 6	. . . . . 6 ⊢ (¬ 𝜒 → (¬ 𝜃 → ¬ 𝜒))
2		falim 1587	. . . . . 6 ⊢ (⊥ → (¬ 𝜃 → ¬ 𝜒))
3	1, 2	ja 188	. . . . 5 ⊢ ((𝜒 → ⊥) → (¬ 𝜃 → ¬ 𝜒))
4	3	imim2i 17	. . . 4 ⊢ (((𝜑 → 𝜓) → (𝜒 → ⊥)) → ((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)))
5	4	imim1i 64	. . 3 ⊢ ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → (((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃))
6	5	imim1i 64	. 2 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏))
7		meredith 1671	. 2 ⊢ (((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))
8	6, 7	syl 18	1 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4  ⊥wfal 1582

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 210  df-tru 1573  df-fal 1583

This theorem is referenced by:  merco1lem1  1744  retbwax2  1746  merco1lem2  1747  merco1lem4  1749  merco1lem5  1750  merco1lem6  1751  merco1lem7  1752  merco1lem10  1756  merco1lem11  1757  merco1lem12  1758  merco1lem13  1759  merco1lem14  1760  merco1lem16  1762  merco1lem17  1763  merco1lem18  1764  retbwax1  1765