| 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 482 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
| 3 | 1, 2 | mto 197 | 1 ⊢ ¬ (𝜑 ∧ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: falantru 1575 rab0 4386 0nelopab 5572 0nelxp 5719 co02 6280 xrltnr 13161 pnfnlt 13170 nltmnf 13171 0nelfz1 13583 smu02 16524 0g0 18677 nolt02o 27740 nogt01o 27741 axlowdimlem13 28969 axlowdimlem16 28972 axlowdim 28976 signstfvneq0 34587 gonanegoal 35357 gonan0 35397 goaln0 35398 fmla0disjsuc 35403 bcneg1 35736 linedegen 36144 epnsymrel 38563 padd02 39814 eldioph4b 42822 iblempty 45980 notatnand 46908 iota0ndef 47051 aiota0ndef 47109 fun2dmnopgexmpl 47296 |
| Copyright terms: Public domain | W3C validator |