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

Theorem pm3.24 870
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 22 . 2  |-  ( ph  ->  ph )
2 iman 424 . 2  |-  ( (
ph  ->  ph )  <->  -.  ( ph  /\  -.  ph )
)
31, 2mpbi 208 1  |-  -.  ( ph  /\  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  pm4.43  911  thema1a  1582  nonconne  2605  pssirr  3444  indifdir  3594  dfnul2  3627  dfnul3  3628  rabnc  3649  axnul  4408  imadif  5481  fiint  7576  kmlem16  8322  zorn2lem4  8656  nnunb  10563  indstr  10911  bwth  18855  lgsquadlem2  22579  ifeqeqx  25726  ballotlemodife  26728  sgn3da  26772  ralnralall  29964  frgrareg  30556  frgraregord013  30557
  Copyright terms: Public domain W3C validator