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 316 | . . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
2 | 1 | imbi2i 337 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓)) |
3 | imnan 400 | . 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
4 | 2, 3 | bitri 276 | 1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: pm3.24 403 annim 404 xor 1008 nic-mpALT 1664 nic-axALT 1666 rexanali 3265 difdif 4106 dfss4 4234 difin 4237 ssdif0 4322 difin0ss 4327 inssdif0 4328 dfif2 4467 notzfausOLD 5255 dffv2 6750 tfinds 7562 domtriord 8652 inf3lem3 9082 nominpos 11863 isprm3 16017 vdwlem13 16319 vdwnn 16324 psgnunilem4 18556 efgredlem 18804 efgred 18805 ufinffr 22467 ptcmplem5 22594 nmoleub2lem2 23649 ellogdm 25149 pntpbnd 26092 cvbr2 29988 cvnbtwn2 29992 cvnbtwn3 29993 cvnbtwn4 29994 chpssati 30068 chrelat2i 30070 chrelat3 30076 bnj1476 32019 bnj110 32030 bnj1388 32203 dff15 32251 df3nandALT1 33645 imnand2 33648 bj-andnotim 33820 lindsenlbs 34769 poimirlem11 34785 poimirlem12 34786 fdc 34903 lpssat 36031 lssat 36034 lcvbr2 36040 lcvbr3 36041 lcvnbtwn2 36045 lcvnbtwn3 36046 cvrval2 36292 cvrnbtwn2 36293 cvrnbtwn3 36294 cvrnbtwn4 36297 atlrelat1 36339 hlrelat2 36421 dihglblem6 38358 dfsucon 39769 or3or 40251 uneqsn 40253 plvcofphax 43064 |
Copyright terms: Public domain | W3C validator |