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

Theorem merco1 1473
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 1400 has 21 symbols, sans parentheses.

See merco2 1496 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 7 . . . . . 6  |-  ( -. 
ch  ->  ( -.  th  ->  -.  ch ) )
2 falim 1325 . . . . . 6  |-  (  F. 
->  ( -.  th  ->  -. 
ch ) )
31, 2ja 155 . . . . 5  |-  ( ( ch  ->  F.  )  ->  ( -.  th  ->  -. 
ch ) )
43imim2i 15 . . . 4  |-  ( ( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  (
( ph  ->  ps )  ->  ( -.  th  ->  -. 
ch ) ) )
54imim1i 56 . . 3  |-  ( ( ( ( ph  ->  ps )  ->  ( -.  th 
->  -.  ch ) )  ->  th )  ->  (
( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  th ) )
65imim1i 56 . 2  |-  ( ( ( ( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  th )  ->  ta )  ->  ( ( ( ( ph  ->  ps )  ->  ( -.  th  ->  -.  ch ) )  ->  th )  ->  ta ) )
7 meredith 1400 . 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 set class
Syntax hints:   -. wn 5    -> wi 6    F. wfal 1313
This theorem is referenced by:  merco1lem1  1474  retbwax2  1476  merco1lem2  1477  merco1lem4  1479  merco1lem5  1480  merco1lem6  1481  merco1lem7  1482  merco1lem10  1486  merco1lem11  1487  merco1lem12  1488  merco1lem13  1489  merco1lem14  1490  merco1lem16  1492  merco1lem17  1493  merco1lem18  1494  retbwax1  1495
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-tru 1315  df-fal 1316
  Copyright terms: Public domain W3C validator