![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > intnanr | Structured version Visualization version GIF 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 476 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
3 | 1, 2 | mto 189 | 1 ⊢ ¬ (𝜑 ∧ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: falantru 1692 rab0 4187 0nelxp 5380 co02 5894 xrltnr 12246 pnfnlt 12255 nltmnf 12256 0nelfz1 12660 smu02 15589 0g0 17623 axlowdimlem13 26260 axlowdimlem16 26263 axlowdim 26267 signstfvneq0 31193 bcneg1 32160 nolt02o 32379 linedegen 32784 epnsymrel 34851 padd02 35882 eldioph4b 38214 iblempty 40969 notatnand 41851 iota0ndef 41964 aiota0ndef 41986 fun2dmnopgexmpl 42181 |
Copyright terms: Public domain | W3C validator |