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

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

See merco2 1510 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 1337 . . . . . 6  |-  (  F. 
->  ( -.  th  ->  -. 
ch ) )
31, 2ja 155 . . . . 5  |-  ( ( ch  ->  F.  )  ->  ( -.  th  ->  -. 
ch ) )
43imim2i 14 . . . 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 1413 . 2  |-  ( ( ( ( ( ph  ->  ps )  ->  ( -.  th  ->  -.  ch )
)  ->  th )  ->  ta )  ->  (
( ta  ->  ph )  ->  ( ch  ->  ph )
) )
86, 7syl 16 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 1326
This theorem is referenced by:  merco1lem1  1488  retbwax2  1490  merco1lem2  1491  merco1lem4  1493  merco1lem5  1494  merco1lem6  1495  merco1lem7  1496  merco1lem10  1500  merco1lem11  1501  merco1lem12  1502  merco1lem13  1503  merco1lem14  1504  merco1lem16  1506  merco1lem17  1507  merco1lem18  1508  retbwax1  1509
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 178  df-tru 1328  df-fal 1329
  Copyright terms: Public domain W3C validator