![]() |
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 4026 axnulALT 4939 axnul 4940 cnv0 5693 imadif 6134 xrltnr 12146 nltmnf 12156 0nelfz1 12553 smu01 15410 3lcm2e6woprm 15530 6lcm4e12 15531 meet0 17338 join0 17339 zringndrg 20040 zclmncvs 23148 legso 25693 rgrx0ndm 26699 wwlksnext 27011 ntrl2v2e 27310 avril1 27630 helloworld 27632 topnfbey 27636 xrge00 29995 dfon2lem7 31999 nolt02o 32151 nandsym1 32727 subsym1 32732 padd01 35600 ifpdfan 38312 clsk1indlem4 38844 iblempty 40684 salexct2 41060 0nodd 42320 2nodd 42322 1neven 42442 |
Copyright terms: Public domain | W3C validator |