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

Theorem pm3.24 853
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 20 . 2  |-  ( ph  ->  ph )
2 iman 414 . 2  |-  ( (
ph  ->  ph )  <->  -.  ( ph  /\  -.  ph )
)
31, 2mpbi 200 1  |-  -.  ( ph  /\  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359
This theorem is referenced by:  pm4.43  894  nonconne  2606  pssirr  3440  indifdir  3590  dfnul2  3623  dfnul3  3624  rabnc  3644  axnul  4330  imadif  5521  fiint  7376  kmlem16  8038  zorn2lem4  8372  nnunb  10210  indstr  10538  lgsquadlem2  21132  ifeqeqx  23994  ballotlemodife  24748
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 178  df-an 361
  Copyright terms: Public domain W3C validator