Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > imnani | Structured version Visualization version GIF version |
Description: Infer implication from 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 437 | . 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) | |
3 | 1, 2 | mpbir 220 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: mptnan 1684 eueq3 3348 onuninsuci 6932 sucprcreg 8389 alephsucdom 8785 pwfseq 9365 eirr 14772 mreexmrid 16126 dvferm1 23552 dvferm2 23554 dchrisumn0 25010 rpvmasum 25015 cvnsym 28533 ballotlem2 29877 bnj1224 30126 bnj1541 30180 bnj1311 30346 bj-imn3ani 31745 |
Copyright terms: Public domain | W3C validator |