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  2419  pssirr  3196  indifdir  3332  dfnul2  3364  dfnul3  3365  rabnc  3385  axnul  4045  imadif  5184  fiint  7018  kmlem16  7675  zorn2lem4  8010  nnunb  9840  indstr  10166  lgsquadlem2  20426  dihglblem6  30219
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