MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  merco1 Structured version   Visualization version   Unicode version

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
StepHypRef Expression
1 ax-1 6 . . . . . 6  |-  ( -. 
ch  ->  ( -.  th  ->  -.  ch ) )
2 falim 1460 . . . . . 6  |-  ( F. 
->  ( -.  th  ->  -. 
ch ) )
31, 2ja 165 . . . . 5  |-  ( ( ch  -> F.  )  ->  ( -.  th  ->  -. 
ch ) )
43imim2i 16 . . . 4  |-  ( ( ( ph  ->  ps )  ->  ( ch  -> F.  ) )  ->  (
( ph  ->  ps )  ->  ( -.  th  ->  -. 
ch ) ) )
54imim1i 60 . . 3  |-  ( ( ( ( ph  ->  ps )  ->  ( -.  th 
->  -.  ch ) )  ->  th )  ->  (
( ( ph  ->  ps )  ->  ( ch  -> F.  ) )  ->  th ) )
65imim1i 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 )
) )
86, 7syl 17 1  |-  ( ( ( ( ( ph  ->  ps )  ->  ( ch  -> F.  ) )  ->  th )  ->  ta )  ->  ( ( ta 
->  ph )  ->  ( ch  ->  ph ) ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator