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  2453  pssirr  3276  indifdir  3425  dfnul2  3457  dfnul3  3458  rabnc  3478  axnul  4148  imadif  5327  fiint  7133  kmlem16  7791  zorn2lem4  8126  nnunb  9961  indstr  10287  lgsquadlem2  20594  ifeqeqx  23034  ballotlemodife  23056  hasheuni  23453  dihglblem6  31530
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