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

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

See merco2 1491 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 5 . . . . . 6  |-  ( -. 
ch  ->  ( -.  th  ->  -.  ch ) )
2 falim 1319 . . . . . 6  |-  (  F. 
->  ( -.  th  ->  -. 
ch ) )
31, 2ja 153 . . . . 5  |-  ( ( ch  ->  F.  )  ->  ( -.  th  ->  -. 
ch ) )
43imim2i 13 . . . 4  |-  ( ( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  (
( ph  ->  ps )  ->  ( -.  th  ->  -. 
ch ) ) )
54imim1i 54 . . 3  |-  ( ( ( ( ph  ->  ps )  ->  ( -.  th 
->  -.  ch ) )  ->  th )  ->  (
( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  th ) )
65imim1i 54 . 2  |-  ( ( ( ( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  th )  ->  ta )  ->  ( ( ( ( ph  ->  ps )  ->  ( -.  th  ->  -.  ch ) )  ->  th )  ->  ta ) )
7 meredith 1394 . 2  |-  ( ( ( ( ( ph  ->  ps )  ->  ( -.  th  ->  -.  ch )
)  ->  th )  ->  ta )  ->  (
( ta  ->  ph )  ->  ( ch  ->  ph )
) )
86, 7syl 15 1  |-  ( ( ( ( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  th )  ->  ta )  ->  ( ( ta 
->  ph )  ->  ( ch  ->  ph ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    F. wfal 1308
This theorem is referenced by:  merco1lem1  1469  retbwax2  1471  merco1lem2  1472  merco1lem4  1474  merco1lem5  1475  merco1lem6  1476  merco1lem7  1477  merco1lem10  1481  merco1lem11  1482  merco1lem12  1483  merco1lem13  1484  merco1lem14  1485  merco1lem16  1487  merco1lem17  1488  merco1lem18  1489  retbwax1  1490
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-fal 1311
  Copyright terms: Public domain W3C validator