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 318 | . . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
2 | 1 | imbi2i 339 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓)) |
3 | imnan 403 | . 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
4 | 2, 3 | bitri 278 | 1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ 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: pm3.24 406 annim 407 xor 1014 nic-mpALT 1679 nic-axALT 1681 rexanali 3176 difdif 4031 dfss4 4159 difin 4162 ssdif0 4262 difin0ss 4267 inssdif0 4268 dfif2 4426 notzfausOLD 5239 dffv2 6775 tfinds 7605 domtriord 8725 inf3lem3 9178 nominpos 11965 isprm3 16136 vdwlem13 16441 vdwnn 16446 psgnunilem4 18755 efgredlem 19003 efgred 19004 ufinffr 22692 ptcmplem5 22819 nmoleub2lem2 23880 ellogdm 25394 pntpbnd 26336 cvbr2 30230 cvnbtwn2 30234 cvnbtwn3 30235 cvnbtwn4 30236 chpssati 30310 chrelat2i 30312 chrelat3 30318 bnj1476 32410 bnj110 32421 bnj1388 32596 dff15 32639 df3nandALT1 34243 imnand2 34246 bj-andnotim 34425 lindsenlbs 35427 poimirlem11 35443 poimirlem12 35444 fdc 35558 lpssat 36682 lssat 36685 lcvbr2 36691 lcvbr3 36692 lcvnbtwn2 36696 lcvnbtwn3 36697 cvrval2 36943 cvrnbtwn2 36944 cvrnbtwn3 36945 cvrnbtwn4 36948 atlrelat1 36990 hlrelat2 37072 dihglblem6 39009 dfsucon 40724 or3or 41217 uneqsn 41219 plvcofphax 44021 ichim 44490 |
Copyright terms: Public domain | W3C validator |