Theorem merco1 1629

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

See merco2 1652 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 1489	. . . . . 6 ⊢ (⊥ → (¬ 𝜃 → ¬ 𝜒))
3	1, 2	ja 172	. . . . 5 ⊢ ((𝜒 → ⊥) → (¬ 𝜃 → ¬ 𝜒))
4	3	imim2i 16	. . . 4 ⊢ (((𝜑 → 𝜓) → (𝜒 → ⊥)) → ((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)))
5	4	imim1i 61	. . 3 ⊢ ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → (((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃))
6	5	imim1i 61	. 2 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏))
7		meredith 1557	. 2 ⊢ (((((𝜑 → 𝜓) → (¬ 𝜃 → ¬ 𝜒)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))
8	6, 7	syl 17	1 ⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))

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

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 196  df-tru 1478  df-fal 1481

This theorem is referenced by:  merco1lem1  1630  retbwax2  1632  merco1lem2  1633  merco1lem4  1635  merco1lem5  1636  merco1lem6  1637  merco1lem7  1638  merco1lem10  1642  merco1lem11  1643  merco1lem12  1644  merco1lem13  1645  merco1lem14  1646  merco1lem16  1648  merco1lem17  1649  merco1lem18  1650  retbwax1  1651