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 476 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑) | |
3 | 1, 2 | mto 187 | 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 196 df-an 385 |
This theorem is referenced by: bianfi 962 indifdir 3842 axnulALT 4715 axnul 4716 cnv0 5454 imadif 5887 xrltnr 11829 nltmnf 11839 0nelfz1 12231 smu01 15046 3lcm2e6woprm 15166 6lcm4e12 15167 meet0 16960 join0 16961 zringndrg 19657 zclmncvs 22756 legso 25294 wwlknext 26252 avril1 26711 helloworld 26713 topnfbey 26717 xrge00 29017 dfon2lem7 30938 nandsym1 31591 subsym1 31596 padd01 34115 ifpdfan 36829 clsk1indlem4 37362 iblempty 38857 salexct2 39233 rgrx0ndm 40793 wwlksnext 41099 ntrl2v2e 41325 0nodd 41600 2nodd 41602 1neven 41722 |
Copyright terms: Public domain | W3C validator |