|   | 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 484 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑) | |
| 3 | 1, 2 | mto 197 | 1 ⊢ ¬ (𝜓 ∧ 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: bianfi 533 noel 4337 axnulALT 5303 axnul 5304 cnv0 6159 imadif 6649 poxp3 8176 1div0 11923 xrltnr 13162 nltmnf 13172 0nelfz1 13584 smu01 16524 3lcm2e6woprm 16653 6lcm4e12 16654 join0 18451 meet0 18452 nsmndex1 18927 smndex2dnrinv 18929 zringndrg 21480 zclmncvs 25183 nolt02o 27741 nogt01o 27742 legso 28608 rgrx0ndm 29612 wwlksnext 29914 ntrl2v2e 30178 avril1 30483 helloworld 30485 topnfbey 30489 xrge00 33018 axsepg2ALT 35098 fmlaomn0 35396 gonan0 35398 goaln0 35399 prv0 35436 dfon2lem7 35791 nandsym1 36424 bj-inftyexpitaudisj 37207 padd01 39814 ifpdfan 43484 sucomisnotcard 43562 clsk1indlem4 44062 iblempty 45985 salexct2 46359 0nodd 48091 2nodd 48093 1neven 48159 ipolub00 48897 | 
| Copyright terms: Public domain | W3C validator |