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  2466  pssirr  3289  indifdir  3438  dfnul2  3470  dfnul3  3471  rabnc  3491  axnul  4164  imadif  5343  fiint  7149  kmlem16  7807  zorn2lem4  8142  nnunb  9977  indstr  10303  lgsquadlem2  20610  ifeqeqx  23050  ballotlemodife  23072  hasheuni  23468  itg2addnc  25005  dihglblem6  32152
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