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 405 | . 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑)) | |
3 | 1, 2 | mpbi 233 | 1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: pm4.43 1022 pssirr 3991 indifdirOLD 4176 dfnul4 4213 dfnul3 4215 dfnul2OLD 4216 dfnul3OLD 4217 noelOLD 4220 rabnc 4276 ralnralall 4405 imadif 6423 fiint 8869 kmlem16 9665 zorn2lem4 9999 nnunb 11972 indstr 12398 bwth 22161 lgsquadlem2 26117 frgrregord013 28332 difrab2 30419 ifeqeqx 30459 ballotlemodife 32034 sgn3da 32078 sbn1ALT 34673 poimirlem30 35430 clsk1indlem4 41200 atnaiana 43957 plcofph 43978 |
Copyright terms: Public domain | W3C validator |