Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > intnanr | Structured version Visualization version Unicode version |
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.) |
Ref | Expression |
---|---|
intnan.1 |
Ref | Expression |
---|---|
intnanr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | intnan.1 | . 2 | |
2 | simpl 473 | . 2 | |
3 | 1, 2 | mto 188 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wa 384 |
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 197 df-an 386 |
This theorem is referenced by: falantru 1508 rab0 3955 rab0OLD 3956 0nelxp 5143 co02 5649 xrltnr 11953 pnfnlt 11962 nltmnf 11963 0nelfz1 12360 smu02 15209 0g0 17263 axlowdimlem13 25834 axlowdimlem16 25837 axlowdim 25841 signstfvneq0 30649 bcneg1 31622 nolt02o 31845 linedegen 32250 padd02 35098 eldioph4b 37375 iblempty 40181 notatnand 41063 fun2dmnopgexmpl 41303 |
Copyright terms: Public domain | W3C validator |