![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > intnan | Structured version Visualization version Unicode 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 467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mto 181 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 df-an 377 |
This theorem is referenced by: bianfi 941 indifdir 3710 axnulALT 4544 axnul 4545 axnulOLD 4546 imadif 5679 xrltnr 11449 nltmnf 11459 0nelfz1 11846 smu01 14508 3lcm2e6woprm 14628 6lcm4e12 14629 meet0 16431 join0 16432 legso 24692 wwlknext 25500 avril1 25948 helloworld 25950 topnfbey 25954 xrge00 28496 dfon2lem7 30483 nandsym1 31130 subsym1 31135 padd01 33420 ifpdfan 36153 iblempty 37879 salexct2 38235 rgrx0ndm 39657 ntrl2v2e 39872 0nodd 40082 2nodd 40084 1neven 40204 |
Copyright terms: Public domain | W3C validator |