Metamath Proof Explorer


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

Proof

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