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

Theorem pm3.24 877
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  918  thema1a  1580  nonconne  2660  pssirr  3567  indifdir  3717  dfnul2  3750  dfnul3  3751  rabnc  3772  axnul  4531  imadif  5604  fiint  7702  kmlem16  8449  zorn2lem4  8783  nnunb  10690  indstr  11038  bwth  19155  lgsquadlem2  22837  ifeqeqx  26081  ballotlemodife  27047  sgn3da  27091  ralnralall  30289  frgrareg  30881  frgraregord013  30882  bj-dfif5ALT  32441
  Copyright terms: Public domain W3C validator