Theorem merco1 1720

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

See merco2 1743 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 1564	. . . . . 6 ⊢ (⊥ → (¬ 𝜃 → ¬ 𝜒))
3	1, 2	ja 187	. . . . 5 ⊢ ((𝜒 → ⊥) → (¬ 𝜃 → ¬ 𝜒))
4	3	imim2i 16	. . . 4 ⊢ (((𝜑 → 𝜓) → (𝜒 → ⊥)) → ((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)))
5	4	imim1i 63	. . 3 ⊢ ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → (((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃))
6	5	imim1i 63	. 2 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏))
7		meredith 1648	. 2 ⊢ (((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))
8	6, 7	syl 17	1 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))

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

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 208  df-tru 1550  df-fal 1560

This theorem is referenced by:  merco1lem1  1721  retbwax2  1723  merco1lem2  1724  merco1lem4  1726  merco1lem5  1727  merco1lem6  1728  merco1lem7  1729  merco1lem10  1733  merco1lem11  1734  merco1lem12  1735  merco1lem13  1736  merco1lem14  1737  merco1lem16  1739  merco1lem17  1740  merco1lem18  1741  retbwax1  1742