| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > imnani | Structured version Visualization version GIF version | ||
| Description: Infer an implication from a negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.) |
| Ref | Expression |
|---|---|
| imnani.1 | ⊢ ¬ (𝜑 ∧ 𝜓) |
| Ref | Expression |
|---|---|
| imnani | ⊢ (𝜑 → ¬ 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imnani.1 | . 2 ⊢ ¬ (𝜑 ∧ 𝜓) | |
| 2 | imnan 399 | . 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) | |
| 3 | 1, 2 | mpbir 231 | 1 ⊢ (𝜑 → ¬ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ 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: mptnan 1768 eueq3 3717 onuninsuci 7861 infn0 9340 sucprcreg 9641 elnotel 9650 alephsucdom 10119 pwfseq 10704 eirr 16241 mreexmrid 17686 dvferm1 26023 dvferm2 26025 dchrisumn0 27565 rpvmasum 27570 cvnsym 32309 ballotlem2 34491 bnj1224 34815 bnj1541 34870 bnj1311 35038 bj-imn3ani 36588 |
| Copyright terms: Public domain | W3C validator |