![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > intnan | Structured version Visualization version GIF version |
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.) |
Ref | Expression |
---|---|
intnan.1 | ⊢ ¬ 𝜑 |
Ref | Expression |
---|---|
intnan | ⊢ ¬ (𝜓 ∧ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | intnan.1 | . 2 ⊢ ¬ 𝜑 | |
2 | simpr 479 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑) | |
3 | 1, 2 | mto 188 | 1 ⊢ ¬ (𝜓 ∧ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: bianfi 1004 indifdir 4027 axnulALT 4940 axnul 4941 cnv0 5694 imadif 6135 xrltnr 12167 nltmnf 12177 0nelfz1 12574 smu01 15431 3lcm2e6woprm 15551 6lcm4e12 15552 meet0 17359 join0 17360 zringndrg 20061 zclmncvs 23169 legso 25715 rgrx0ndm 26721 wwlksnext 27033 ntrl2v2e 27332 avril1 27652 helloworld 27654 topnfbey 27658 xrge00 30017 dfon2lem7 32021 nolt02o 32173 nandsym1 32749 subsym1 32754 padd01 35619 ifpdfan 38331 clsk1indlem4 38863 iblempty 40703 salexct2 41079 0nodd 42339 2nodd 42341 1neven 42461 |
Copyright terms: Public domain | W3C validator |