Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > notnotb | Structured version Visualization version GIF version |
Description: Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.) |
Ref | Expression |
---|---|
notnotb | ⊢ (𝜑 ↔ ¬ ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot 144 | . 2 ⊢ (𝜑 → ¬ ¬ 𝜑) | |
2 | notnotr 132 | . 2 ⊢ (¬ ¬ 𝜑 → 𝜑) | |
3 | 1, 2 | impbii 210 | 1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 |
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 |
This theorem is referenced by: notbid 319 jcn 338 con2bi 355 con1bii 358 con2bii 359 iman 402 imor 847 anor 976 ifpn 1064 noranOLD 1518 nororOLD 1520 alex 1817 nfnbi 1846 necon1abid 3054 necon4abid 3056 necon2abid 3058 necon2bbid 3059 necon1abii 3064 dfral2 3237 ralnex2OLD 3261 ralnex3OLD 3263 dfss6 3956 falseral0 4457 difsnpss 4734 xpimasn 6036 2mpo0 7383 bropfvvvv 7778 zfregs2 9164 nqereu 10340 ssnn0fi 13343 swrdnnn0nd 14008 pfxnd0 14040 zeo4 15677 sumodd 15729 ncoprmlnprm 16058 numedglnl 26857 ballotlemfc0 31650 ballotlemfcc 31651 bnj1143 31962 bnj1304 31991 bnj1189 32179 tsim1 35291 tsna1 35305 ecinn0 35490 ifpxorcor 39722 ifpnot23b 39728 ifpnot23c 39730 ifpnot23d 39731 iunrelexp0 39927 expandrex 40508 con5VD 41114 sineq0ALT 41151 nepnfltpnf 41490 nemnftgtmnft 41492 sge0gtfsumgt 42606 atbiffatnnb 43029 ichnreuop 43481 islininds2 44437 nnolog2flm1 44548 line2ylem 44636 |
Copyright terms: Public domain | W3C validator |