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 488 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑) | |
3 | 1, 2 | mto 200 | 1 ⊢ ¬ (𝜓 ∧ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: bianfi 537 indifdirOLD 4174 noel 4217 noelOLD 4218 dfopif 4752 axnulALT 5169 axnul 5170 cnv0 5967 imadif 6417 xrltnr 12590 nltmnf 12600 0nelfz1 13010 smu01 15922 3lcm2e6woprm 16049 6lcm4e12 16050 meet0 17856 join0 17857 nsmndex1 18187 smndex2dnrinv 18189 zringndrg 20302 zclmncvs 23893 legso 26537 rgrx0ndm 27527 wwlksnext 27823 ntrl2v2e 28087 avril1 28392 helloworld 28394 topnfbey 28398 xrge00 30864 fmlaomn0 32915 gonan0 32917 goaln0 32918 prv0 32955 dfon2lem7 33329 poxp3 33399 nolt02o 33531 nogt01o 33532 nandsym1 34241 subsym1 34246 bj-inftyexpitaudisj 34986 padd01 37437 ifpdfan 40611 clsk1indlem4 41184 iblempty 43032 salexct2 43404 0nodd 44882 2nodd 44884 1neven 45008 |
Copyright terms: Public domain | W3C validator |