![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iman | Structured version Visualization version GIF version |
Description: Implication in terms of conjunction and negation. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.) |
Ref | Expression |
---|---|
iman | ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb 307 | . . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
2 | 1 | imbi2i 328 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓)) |
3 | imnan 389 | . 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
4 | 2, 3 | bitri 267 | 1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 385 |
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 386 |
This theorem is referenced by: pm3.24 392 annim 393 xor 1039 nic-mpALT 1768 nic-axALT 1770 rexanali 3178 difdif 3934 dfss4 4059 difin 4062 ssdif0 4142 difin0ss 4147 inssdif0 4148 dfif2 4279 notzfaus 5032 dffv2 6496 tfinds 7293 domtriord 8348 inf3lem3 8777 nominpos 11557 isprm3 15730 vdwlem13 16030 vdwnn 16035 psgnunilem4 18230 efgredlem 18474 efgredlemOLD 18475 efgred 18476 ufinffr 22061 ptcmplem5 22188 nmoleub2lem2 23243 ellogdm 24726 pntpbnd 25629 cvbr2 29667 cvnbtwn2 29671 cvnbtwn3 29672 cvnbtwn4 29673 chpssati 29747 chrelat2i 29749 chrelat3 29755 bnj1476 31434 bnj110 31445 bnj1388 31618 df3nandALT1 32906 imnand2 32909 bj-andnotim 33078 lindsenlbs 33893 poimirlem11 33909 poimirlem12 33910 fdc 34028 lpssat 35034 lssat 35037 lcvbr2 35043 lcvbr3 35044 lcvnbtwn2 35048 lcvnbtwn3 35049 cvrval2 35295 cvrnbtwn2 35296 cvrnbtwn3 35297 cvrnbtwn4 35300 atlrelat1 35342 hlrelat2 35424 dihglblem6 37361 or3or 39097 uneqsn 39099 plvcofphax 41856 |
Copyright terms: Public domain | W3C validator |