HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Axiom ax-3 6
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.
Assertion
Ref Expression
ax-3 |- ((-. ph -> -. ps) -> (ps -> ph))

Detailed syntax breakdown of Axiom ax-3
StepHypRef Expression
1 wph . . . 4 wff ph
21wn 2 . . 3 wff -. ph
3 wps . . . 4 wff ps
43wn 2 . . 3 wff -. ps
52, 4wi 3 . 2 wff (-. ph -> -. ps)
63, 1wi 3 . 2 wff (ps -> ph)
75, 6wi 3 1 wff ((-. ph -> -. ps) -> (ps -> ph))
Colors of variables: wff set class
This axiom is referenced by:  con4i 125  con4d 126  dfbi1gb 239  con34b 355  meredith 1503  meredithOLDOLD 1505  notnot2ALTVD 17822  con3ALTVD 17823
Copyright terms: Public domain