![]() |
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 474 | . 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 1657 rab0 4098 rab0OLD 4099 0nelxp 5300 co02 5810 xrltnr 12146 pnfnlt 12155 nltmnf 12156 0nelfz1 12553 smu02 15411 0g0 17464 axlowdimlem13 26033 axlowdimlem16 26036 axlowdim 26040 signstfvneq0 30958 bcneg1 31929 nolt02o 32151 linedegen 32556 epnsymrel 34631 padd02 35601 eldioph4b 37877 iblempty 40684 notatnand 41569 fun2dmnopgexmpl 41811 |
Copyright terms: Public domain | W3C validator |