![]() |
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 390 | . 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) | |
3 | 1, 2 | mpbir 223 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: mptnan 1812 eueq3 3593 onuninsuci 7320 sucprcreg 8797 elnotel 8804 alephsucdom 9237 pwfseq 9823 eirr 15346 mreexmrid 16700 dvferm1 24196 dvferm2 24198 dchrisumn0 25679 rpvmasum 25684 cvnsym 29738 ballotlem2 31157 bnj1224 31479 bnj1541 31533 bnj1311 31699 bj-imn3ani 33159 |
Copyright terms: Public domain | W3C validator |