![]() |
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 398 | . 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) | |
3 | 1, 2 | mpbir 230 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ 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: mptnan 1762 eueq3 3703 onuninsuci 7845 infn0 9335 sucprcreg 9631 elnotel 9640 alephsucdom 10109 pwfseq 10694 eirr 16193 mreexmrid 17642 dvferm1 25978 dvferm2 25980 dchrisumn0 27519 rpvmasum 27524 cvnsym 32192 ballotlem2 34259 bnj1224 34583 bnj1541 34638 bnj1311 34806 bj-imn3ani 36215 |
Copyright terms: Public domain | W3C validator |