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

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

See merco2 1569 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

Proof of Theorem merco1
StepHypRef Expression
1 ax-1 6 . . . . . 6
2 falim 1409 . . . . . 6
31, 2ja 161 . . . . 5
43imim2i 14 . . . 4
54imim1i 58 . . 3
65imim1i 58 . 2
7 meredith 1472 . 2
86, 7syl 16 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4   wfal 1400
This theorem is referenced by:  merco1lem1  1547  retbwax2  1549  merco1lem2  1550  merco1lem4  1552  merco1lem5  1553  merco1lem6  1554  merco1lem7  1555  merco1lem10  1559  merco1lem11  1560  merco1lem12  1561  merco1lem13  1562  merco1lem14  1563  merco1lem16  1565  merco1lem17  1566  merco1lem18  1567  retbwax1  1568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-tru 1398  df-fal 1401
  Copyright terms: Public domain W3C validator