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

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

See merco2 1492 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 1321 . . . . . 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 1396 . 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 1310
This theorem is referenced by:  merco1lem1  1470  retbwax2  1472  merco1lem2  1473  merco1lem4  1475  merco1lem5  1476  merco1lem6  1477  merco1lem7  1478  merco1lem10  1482  merco1lem11  1483  merco1lem12  1484  merco1lem13  1485  merco1lem14  1486  merco1lem16  1488  merco1lem17  1489  merco1lem18  1490  retbwax1  1491
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 1312  df-fal 1313
  Copyright terms: Public domain W3C validator