![]() |
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 481 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
3 | 1, 2 | mto 196 | 1 ⊢ ¬ (𝜑 ∧ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: falantru 1568 rab0 4384 0nelopab 5571 0nelxp 5714 co02 6267 xrltnr 13137 pnfnlt 13146 nltmnf 13147 0nelfz1 13558 smu02 16467 0g0 18629 nolt02o 27646 nogt01o 27647 axlowdimlem13 28783 axlowdimlem16 28786 axlowdim 28790 signstfvneq0 34209 gonanegoal 34967 gonan0 35007 goaln0 35008 fmla0disjsuc 35013 bcneg1 35335 linedegen 35744 epnsymrel 38038 padd02 39289 eldioph4b 42234 iblempty 45355 notatnand 46280 iota0ndef 46423 aiota0ndef 46479 fun2dmnopgexmpl 46666 |
Copyright terms: Public domain | W3C validator |