Theorem merco1 1478

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

See merco2 1501 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 1328	. . . . . 6 ⊢ ( ⊥ → (¬ θ → ¬ χ))
3	1, 2	ja 153	. . . . 5 ⊢ ((χ → ⊥ ) → (¬ θ → ¬ χ))
4	3	imim2i 13	. . . 4 ⊢ (((φ → ψ) → (χ → ⊥ )) → ((φ → ψ) → (¬ θ → ¬ χ)))
5	4	imim1i 54	. . 3 ⊢ ((((φ → ψ) → (¬ θ → ¬ χ)) → θ) → (((φ → ψ) → (χ → ⊥ )) → θ))
6	5	imim1i 54	. 2 ⊢ (((((φ → ψ) → (χ → ⊥ )) → θ) → τ) → ((((φ → ψ) → (¬ θ → ¬ χ)) → θ) → τ))
7		meredith 1404	. 2 ⊢ (((((φ → ψ) → (¬ θ → ¬ χ)) → θ) → τ) → ((τ → φ) → (χ → φ)))
8	6, 7	syl 15	1 ⊢ (((((φ → ψ) → (χ → ⊥ )) → θ) → τ) → ((τ → φ) → (χ → φ)))

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

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 177  df-tru 1319  df-fal 1320

This theorem is referenced by:  merco1lem1  1479  retbwax2  1481  merco1lem2  1482  merco1lem4  1484  merco1lem5  1485  merco1lem6  1486  merco1lem7  1487  merco1lem10  1491  merco1lem11  1492  merco1lem12  1493  merco1lem13  1494  merco1lem14  1495  merco1lem16  1497  merco1lem17  1498  merco1lem18  1499  retbwax1  1500