merco1

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

See merco2 for another axiom of equal length. (Contributed by Anthony Hart, 13-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	merco1	$⊢ ((((φ \to ψ) \to (χ \to ⊥)) \to θ) \to τ) \to ((τ \to φ) \to (χ \to φ))$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$⊢ \neg χ \to (\neg θ \to \neg χ)$
2		falim	$⊢ ⊥ \to (\neg θ \to \neg χ)$
3	1 2	ja	$⊢ (χ \to ⊥) \to (\neg θ \to \neg χ)$
4	3	imim2i	$⊢ ((φ \to ψ) \to (χ \to ⊥)) \to ((φ \to ψ) \to (\neg θ \to \neg χ))$
5	4	imim1i	$⊢ (((φ \to ψ) \to (\neg θ \to \neg χ)) \to θ) \to (((φ \to ψ) \to (χ \to ⊥)) \to θ)$
6	5	imim1i	$⊢ ((((φ \to ψ) \to (χ \to ⊥)) \to θ) \to τ) \to ((((φ \to ψ) \to (\neg θ \to \neg χ)) \to θ) \to τ)$
7		meredith	$⊢ ((((φ \to ψ) \to (\neg θ \to \neg χ)) \to θ) \to τ) \to ((τ \to φ) \to (χ \to φ))$
8	6 7	syl	$⊢ ((((φ \to ψ) \to (χ \to ⊥)) \to θ) \to τ) \to ((τ \to φ) \to (χ \to φ))$

Metamath Proof Explorer

Theorem merco1

Proof