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 400 | . 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) | |
3 | 1, 2 | mpbir 232 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: mptnan 1760 eueq3 3701 onuninsuci 7543 sucprcreg 9054 elnotel 9062 alephsucdom 9494 pwfseq 10075 eirr 15548 mreexmrid 16904 dvferm1 24511 dvferm2 24513 dchrisumn0 26025 rpvmasum 26030 cvnsym 29995 ballotlem2 31646 bnj1224 31973 bnj1541 32028 bnj1311 32194 bj-imn3ani 33819 |
Copyright terms: Public domain | W3C validator |