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

Theorem pm3.24 890
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 425 . 2  |-  ( (
ph  ->  ph )  <->  -.  ( ph  /\  -.  ph )
)
31, 2mpbi 211 1  |-  -.  ( ph  /\  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm4.43  935  stoic1aOLD  1650  nonconneOLD  2613  pssirr  3508  indifdir  3672  dfnul2  3706  dfnul3  3707  rabnc  3729  axnulOLD  4497  imadif  5619  fiint  7801  kmlem16  8546  zorn2lem4  8880  nnunb  10816  indstr  11178  bwth  20367  lgsquadlem2  24225  frgrareg  25787  frgraregord013  25788  ifeqeqx  28104  ballotlemodife  29282  sgn3da  29364  poimirlem30  31877  atnaiana  38325  plcofph  38346  ralnralall  38796
  Copyright terms: Public domain W3C validator