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 229 | 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 206 df-an 397 |
This theorem is referenced by: pm4.43 1020 pssirr 4035 indifdirOLD 4219 dfnul4 4258 dfnul3 4260 dfnul2OLD 4261 dfnul3OLD 4262 noelOLD 4265 rabnc 4321 ralnralall 4449 imadif 6518 fiint 9091 kmlem16 9921 zorn2lem4 10255 nnunb 12229 indstr 12656 bwth 22561 lgsquadlem2 26529 frgrregord013 28759 difrab2 30845 ifeqeqx 30885 ballotlemodife 32464 sgn3da 32508 sbn1ALT 35042 poimirlem30 35807 clsk1indlem4 41654 atnaiana 44418 plcofph 44439 |
Copyright terms: Public domain | W3C validator |