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  thema1a  1589  nonconneOLD  2676  pssirr  3609  indifdir  3759  dfnul2  3792  dfnul3  3793  rabnc  3814  axnul  4580  imadif  5668  fiint  7807  kmlem16  8555  zorn2lem4  8889  nnunb  10801  indstr  11160  bwth  19755  lgsquadlem2  23473  frgrareg  24909  frgraregord013  24910  ifeqeqx  27210  ballotlemodife  28229  sgn3da  28273  ralnralall  32052  bj-dfif5ALT  33523
  Copyright terms: Public domain W3C validator