Theorem merco1 1638

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

See merco2 1661 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	|- ( ( ( ( ( ph -> ps ) -> ( ch -> F. ) ) -> th ) -> ta ) -> ( ( ta -> ph ) -> ( ch -> ph ) ) )

Proof of Theorem merco1

Step	Hyp	Ref	Expression
1		ax-1 6	. . . . . 6 |- ( -. ch -> ( -. th -> -. ch ) )
2		falim 1498	. . . . . 6 |- ( F. -> ( -. th -> -. ch ) )
3	1, 2	ja 173	. . . . 5 |- ( ( ch -> F. ) -> ( -. th -> -. ch ) )
4	3	imim2i 16	. . . 4 |- ( ( ( ph -> ps ) -> ( ch -> F. ) ) -> ( ( ph -> ps ) -> ( -. th -> -. ch ) ) )
5	4	imim1i 63	. . 3 |- ( ( ( ( ph -> ps ) -> ( -. th -> -. ch ) ) -> th ) -> ( ( ( ph -> ps ) -> ( ch -> F. ) ) -> th ) )
6	5	imim1i 63	. 2 |- ( ( ( ( ( ph -> ps ) -> ( ch -> F. ) ) -> th ) -> ta ) -> ( ( ( ( ph -> ps ) -> ( -. th -> -. ch ) ) -> th ) -> ta ) )
7		meredith 1566	. 2 |- ( ( ( ( ( ph -> ps ) -> ( -. th -> -. ch ) ) -> th ) -> ta ) -> ( ( ta -> ph ) -> ( ch -> ph ) ) )
8	6, 7	syl 17	1 |- ( ( ( ( ( ph -> ps ) -> ( ch -> F. ) ) -> th ) -> ta ) -> ( ( ta -> ph ) -> ( ch -> ph ) ) )

Syntax hints:   -. wn 3   -> wi 4   F. wfal 1488

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 197  df-tru 1486  df-fal 1489

This theorem is referenced by:  merco1lem1  1639  retbwax2  1641  merco1lem2  1642  merco1lem4  1644  merco1lem5  1645  merco1lem6  1646  merco1lem7  1647  merco1lem10  1651  merco1lem11  1652  merco1lem12  1653  merco1lem13  1654  merco1lem14  1655  merco1lem16  1657  merco1lem17  1658  merco1lem18  1659  retbwax1  1660