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  2428  pssirr  3251  indifdir  3400  dfnul2  3432  dfnul3  3433  rabnc  3453  axnul  4122  imadif  5265  fiint  7101  kmlem16  7759  zorn2lem4  8094  nnunb  9929  indstr  10255  lgsquadlem2  20557  ifeqeqx  22995  ballotlemodife  23018  dihglblem6  30780
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