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 402 | . 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑)) | |
3 | 1, 2 | mpbi 231 | 1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: pm4.43 1016 pssirr 4076 indifdir 4259 dfnul2 4292 dfnul2OLD 4293 dfnul3 4294 noel 4295 rabnc 4340 ralnralall 4456 imadif 6432 fiint 8784 kmlem16 9580 zorn2lem4 9910 nnunb 11882 indstr 12305 bwth 21948 lgsquadlem2 25885 frgrregord013 28102 difrab2 30189 ifeqeqx 30225 ballotlemodife 31655 sgn3da 31699 poimirlem30 34804 clsk1indlem4 40274 atnaiana 43040 plcofph 43061 |
Copyright terms: Public domain | W3C validator |