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

Axiom ax-3 8
Description: Axiom Transp. Axiom A3 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It swaps or "transposes" the order of the consequents when negation is removed. An informal example is that the statement "if there are no clouds in the sky, it is not raining" implies the statement "if it is raining, there are clouds in the sky." This axiom is called Transp or "the principle of transposition" in Principia Mathematica (Theorem *2.17 of [WhiteheadRussell] p. 103). We will also use the term "contraposition" for this principle, although the reader is advised that in the field of philosophical logic, "contraposition" has a different technical meaning. (Contributed by NM, 30-Sep-1992.)
Assertion
Ref Expression
ax-3

Detailed syntax breakdown of Axiom ax-3
StepHypRef Expression
1 wph . . . 4
21wn 3 . . 3
3 wps . . . 4
43wn 3 . . 3
52, 4wi 4 . 2
63, 1wi 4 . 2
75, 6wi 4 1
Colors of variables: wff setvar class
This axiom is referenced by:  con4d  105  dfbi1ALT  193  con34b  292  meredith  1472  notnot2ALTVD  33715  con3ALTVD  33716  bj-con4iALT  34138  frege54cor0a  37890
  Copyright terms: Public domain W3C validator