Theorem merco1 1740

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

See merco2 1763 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 1584	. . . . . 6 ⊢ (⊥ → (¬ 𝜃 → ¬ 𝜒))
3	1, 2	ja 188	. . . . 5 ⊢ ((𝜒 → ⊥) → (¬ 𝜃 → ¬ 𝜒))
4	3	imim2i 17	. . . 4 ⊢ (((𝜑 → 𝜓) → (𝜒 → ⊥)) → ((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)))
5	4	imim1i 64	. . 3 ⊢ ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → (((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃))
6	5	imim1i 64	. 2 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏))
7		meredith 1668	. 2 ⊢ (((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))
8	6, 7	syl 18	1 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))

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

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 1570  df-fal 1580

This theorem is referenced by:  merco1lem1  1741  retbwax2  1743  merco1lem2  1744  merco1lem4  1746  merco1lem5  1747  merco1lem6  1748  merco1lem7  1749  merco1lem10  1753  merco1lem11  1754  merco1lem12  1755  merco1lem13  1756  merco1lem14  1757  merco1lem16  1759  merco1lem17  1760  merco1lem18  1761  retbwax1  1762