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 403 | . 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) | |
3 | 1, 2 | mpbir 234 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: mptnan 1776 eueq3 3624 onuninsuci 7619 sucprcreg 9217 elnotel 9225 alephsucdom 9693 pwfseq 10278 eirr 15766 mreexmrid 17146 dvferm1 24882 dvferm2 24884 dchrisumn0 26402 rpvmasum 26407 cvnsym 30371 ballotlem2 32167 bnj1224 32494 bnj1541 32549 bnj1311 32717 bj-imn3ani 34506 |
Copyright terms: Public domain | W3C validator |