Theorem merco1 1598

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

See merco2 1621 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 1460	. . . . . 6 |- ( F. -> ( -. th -> -. ch ) )
3	1, 2	ja 165	. . . . 5 |- ( ( ch -> F. ) -> ( -. th -> -. ch ) )
4	3	imim2i 16	. . . 4 |- ( ( ( ph -> ps ) -> ( ch -> F. ) ) -> ( ( ph -> ps ) -> ( -. th -> -. ch ) ) )
5	4	imim1i 60	. . 3 |- ( ( ( ( ph -> ps ) -> ( -. th -> -. ch ) ) -> th ) -> ( ( ( ph -> ps ) -> ( ch -> F. ) ) -> th ) )
6	5	imim1i 60	. 2 |- ( ( ( ( ( ph -> ps ) -> ( ch -> F. ) ) -> th ) -> ta ) -> ( ( ( ( ph -> ps ) -> ( -. th -> -. ch ) ) -> th ) -> ta ) )
7		meredith 1526	. 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 1451

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 189  df-tru 1449  df-fal 1452

This theorem is referenced by:  merco1lem1  1599  retbwax2  1601  merco1lem2  1602  merco1lem4  1604  merco1lem5  1605  merco1lem6  1606  merco1lem7  1607  merco1lem10  1611  merco1lem11  1612  merco1lem12  1613  merco1lem13  1614  merco1lem14  1615  merco1lem16  1617  merco1lem17  1618  merco1lem18  1619  retbwax1  1620