![]() |
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 472 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
3 | 1, 2 | mto 188 | 1 ⊢ ¬ (𝜑 ∧ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 383 |
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 385 |
This theorem is referenced by: falantru 1548 rab0 3988 rab0OLD 3989 0nelxp 5177 co02 5687 xrltnr 11991 pnfnlt 12000 nltmnf 12001 0nelfz1 12398 smu02 15256 0g0 17310 axlowdimlem13 25879 axlowdimlem16 25882 axlowdim 25886 signstfvneq0 30777 bcneg1 31748 nolt02o 31970 linedegen 32375 padd02 35416 eldioph4b 37692 iblempty 40499 notatnand 41384 fun2dmnopgexmpl 41626 |
Copyright terms: Public domain | W3C validator |