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

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

See merco2 1511 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 1338 . . . . . 6  |-  (  F. 
->  ( -.  th  ->  -. 
ch ) )
31, 2ja 156 . . . . 5  |-  ( ( ch  ->  F.  )  ->  ( -.  th  ->  -. 
ch ) )
43imim2i 14 . . . 4  |-  ( ( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  (
( ph  ->  ps )  ->  ( -.  th  ->  -. 
ch ) ) )
54imim1i 57 . . 3  |-  ( ( ( ( ph  ->  ps )  ->  ( -.  th 
->  -.  ch ) )  ->  th )  ->  (
( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  th ) )
65imim1i 57 . 2  |-  ( ( ( ( ( ph  ->  ps )  ->  ( ch  ->  F.  ) )  ->  th )  ->  ta )  ->  ( ( ( ( ph  ->  ps )  ->  ( -.  th  ->  -.  ch ) )  ->  th )  ->  ta ) )
7 meredith 1414 . 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 1327
This theorem is referenced by:  merco1lem1  1489  retbwax2  1491  merco1lem2  1492  merco1lem4  1494  merco1lem5  1495  merco1lem6  1496  merco1lem7  1497  merco1lem10  1501  merco1lem11  1502  merco1lem12  1503  merco1lem13  1504  merco1lem14  1505  merco1lem16  1507  merco1lem17  1508  merco1lem18  1509  retbwax1  1510
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 179  df-tru 1329  df-fal 1330
  Copyright terms: Public domain W3C validator