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

Theorem pm3.24 857
Description: Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Assertion
Ref Expression
pm3.24  |-  -.  ( ph  /\  -.  ph )

Proof of Theorem pm3.24
StepHypRef Expression
1 id 21 . 2  |-  ( ph  ->  ph )
2 iman 415 . 2  |-  ( (
ph  ->  ph )  <->  -.  ( ph  /\  -.  ph )
)
31, 2mpbi 201 1  |-  -.  ( ph  /\  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    /\ wa 360
This theorem is referenced by:  pm4.43  898  nonconne  2426  pssirr  3218  indifdir  3367  dfnul2  3399  dfnul3  3400  rabnc  3420  axnul  4088  imadif  5230  fiint  7066  kmlem16  7724  zorn2lem4  8059  nnunb  9893  indstr  10219  lgsquadlem2  20521  ifeqeqx  22959  ballotlemodife  22982  dihglblem6  30660
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-an 362
  Copyright terms: Public domain W3C validator