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

Theorem pm3.24 880
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  925  stoic1a  1590  nonconneOLD  2650  pssirr  3586  indifdir  3736  dfnul2  3769  dfnul3  3770  rabnc  3791  axnul  4561  imadif  5649  fiint  7795  kmlem16  8543  zorn2lem4  8877  nnunb  10792  indstr  11154  bwth  19776  lgsquadlem2  23495  frgrareg  24982  frgraregord013  24983  ifeqeqx  27284  ballotlemodife  28302  sgn3da  28346  ralnralall  32128  bj-dfif5ALT  33863
  Copyright terms: Public domain W3C validator