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 315 | . . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
2 | 1 | imbi2i 336 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓)) |
3 | imnan 400 | . 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
4 | 2, 3 | bitri 274 | 1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ 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 206 df-an 397 |
This theorem is referenced by: pm3.24 403 annim 404 xor 1012 nic-mpALT 1675 nic-axALT 1677 rexanali 3192 difdif 4065 dfss4 4192 difin 4195 ssdif0 4297 difin0ss 4302 inssdif0 4303 dfif2 4461 dffv2 6863 tfinds 7706 sdom0 8895 domtriord 8910 inf3lem3 9388 nominpos 12210 isprm3 16388 vdwlem13 16694 vdwnn 16699 psgnunilem4 19105 efgredlem 19353 efgred 19354 ufinffr 23080 ptcmplem5 23207 nmoleub2lem2 24279 ellogdm 25794 pntpbnd 26736 cvbr2 30645 cvnbtwn2 30649 cvnbtwn3 30650 cvnbtwn4 30651 chpssati 30725 chrelat2i 30727 chrelat3 30733 bnj1476 32827 bnj110 32838 bnj1388 33013 dff15 33056 df3nandALT1 34588 imnand2 34591 bj-andnotim 34770 lindsenlbs 35772 poimirlem11 35788 poimirlem12 35789 fdc 35903 lpssat 37027 lssat 37030 lcvbr2 37036 lcvbr3 37037 lcvnbtwn2 37041 lcvnbtwn3 37042 cvrval2 37288 cvrnbtwn2 37289 cvrnbtwn3 37290 cvrnbtwn4 37293 atlrelat1 37335 hlrelat2 37417 dihglblem6 39354 dfsucon 41130 or3or 41631 uneqsn 41633 plvcofphax 44442 ichim 44909 |
Copyright terms: Public domain | W3C validator |