|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > pm3.24 | Structured version Visualization version GIF version | ||
| 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.) | 
| Ref | Expression | 
|---|---|
| pm3.24 | ⊢ ¬ (𝜑 ∧ ¬ 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
| 2 | iman 401 | . 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑)) | |
| 3 | 1, 2 | mpbi 230 | 1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: pm4.43 1024 pssirr 4102 dfnul4 4334 dfnul3 4336 rabnc 4390 ralnralall 4514 imadif 6649 fiint 9367 fiintOLD 9368 kmlem16 10207 zorn2lem4 10540 nnunb 12524 indstr 12959 bwth 23419 lgsquadlem2 27426 frgrregord013 30415 difrab2 32518 ifeqeqx 32556 ballotlemodife 34501 sgn3da 34545 sbn1ALT 36860 poimirlem30 37658 clsk1indlem4 44062 atnaiana 46940 plcofph 46961 | 
| Copyright terms: Public domain | W3C validator |