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 485 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑) | |
3 | 1, 2 | mto 196 | 1 ⊢ ¬ (𝜓 ∧ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: bianfi 534 indifdirOLD 4220 noel 4265 noelOLD 4266 dfopif 4801 axnulALT 5229 axnul 5230 cnv0 6049 imadif 6525 xrltnr 12864 nltmnf 12874 0nelfz1 13284 smu01 16202 3lcm2e6woprm 16329 6lcm4e12 16330 join0 18132 meet0 18133 nsmndex1 18561 smndex2dnrinv 18563 zringndrg 20699 zclmncvs 24321 legso 26969 rgrx0ndm 27969 wwlksnext 28267 ntrl2v2e 28531 avril1 28836 helloworld 28838 topnfbey 28842 xrge00 31304 fmlaomn0 33361 gonan0 33363 goaln0 33364 prv0 33401 dfon2lem7 33774 poxp3 33805 nolt02o 33907 nogt01o 33908 nandsym1 34620 subsym1 34625 bj-inftyexpitaudisj 35385 padd01 37832 ifpdfan 41080 sucomisnotcard 41158 clsk1indlem4 41661 iblempty 43513 salexct2 43885 0nodd 45375 2nodd 45377 1neven 45501 ipolub00 46290 |
Copyright terms: Public domain | W3C validator |