Theorem merco1 1733

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

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

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

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 209  df-tru 1563  df-fal 1573

This theorem is referenced by:  merco1lem1  1734  retbwax2  1736  merco1lem2  1737  merco1lem4  1739  merco1lem5  1740  merco1lem6  1741  merco1lem7  1742  merco1lem10  1746  merco1lem11  1747  merco1lem12  1748  merco1lem13  1749  merco1lem14  1750  merco1lem16  1752  merco1lem17  1753  merco1lem18  1754  retbwax1  1755