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

Theorem pm3.24 852
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 19 . 2  |-  ( ph  ->  ph )
2 iman 413 . 2  |-  ( (
ph  ->  ph )  <->  -.  ( ph  /\  -.  ph )
)
31, 2mpbi 199 1  |-  -.  ( ph  /\  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358
This theorem is referenced by:  pm4.43  893  nonconne  2455  pssirr  3278  indifdir  3427  dfnul2  3459  dfnul3  3460  rabnc  3480  axnul  4150  imadif  5329  fiint  7135  kmlem16  7793  zorn2lem4  8128  nnunb  9963  indstr  10289  lgsquadlem2  20596  ifeqeqx  23036  ballotlemodife  23058  hasheuni  23455  itg2addnc  24935  dihglblem6  31603
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator