Metamath Proof Explorer


Table of Contents - 20.16.1. Propositional calculus

Miscellaneous utility theorems of propositional calculus.

  1. Derived rules of inference
    1. bj-mp2c
    2. bj-mp2d
  2. A syntactic theorem
    1. bj-0
    2. bj-1
  3. Minimal implicational calculus
    1. bj-a1k
    2. bj-nnclav
    3. bj-jarrii
    4. bj-imim21
    5. bj-imim21i
    6. bj-peircestab
    7. bj-stabpeirce
  4. Positive calculus
    1. bj-syl66ib
    2. bj-orim2
    3. bj-currypeirce
    4. bj-peircecurry
    5. bj-animbi
    6. bj-currypara
  5. Implication and negation
    1. bj-con2com
    2. bj-con2comi
    3. bj-pm2.01i
    4. bj-nimn
    5. bj-nimni
    6. bj-peircei
    7. bj-looinvi
    8. bj-looinvii
  6. Disjunction
    1. bj-jaoi1
    2. bj-jaoi2
  7. Logical equivalence
    1. bj-dfbi4
    2. bj-dfbi5
    3. bj-dfbi6
    4. bj-bijust0ALT
    5. bj-bijust00
  8. The conditional operator for propositions
    1. bj-consensus
    2. bj-consensusALT
    3. bj-df-ifc
    4. bj-dfif
    5. bj-ififc
  9. Propositional calculus: miscellaneous
    1. bj-imbi12
    2. bj-biorfi
    3. bj-falor
    4. bj-falor2
    5. bj-bibibi
    6. bj-imn3ani
    7. bj-andnotim
    8. bj-bi3ant
    9. bj-bisym
    10. bj-bixor