![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con1bii | Structured version Visualization version GIF version |
Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.) |
Ref | Expression |
---|---|
con1bii.1 | ⊢ (¬ 𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
con1bii | ⊢ (¬ 𝜓 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb 304 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | con1bii.1 | . . 3 ⊢ (¬ 𝜑 ↔ 𝜓) | |
3 | 1, 2 | xchbinx 323 | . 2 ⊢ (𝜑 ↔ ¬ 𝜓) |
4 | 3 | bicomi 214 | 1 ⊢ (¬ 𝜓 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 |
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 197 |
This theorem is referenced by: con2bii 346 xor 971 3anor 1097 3oran 1099 2nexaln 1898 nnel 3036 npss 3851 symdifass 3988 dfnul3 4053 snprc 4389 dffv2 6425 kmlem3 9158 axpowndlem3 9605 nnunb 11472 rpnnen2lem12 15145 dsmmacl 20279 ntreq0 21075 largei 29427 spc2d 29614 ballotlem2 30851 dffr5 31942 noetalem3 32163 brsset 32294 brtxpsd 32299 dfrecs2 32355 dfint3 32357 con1bii2 33482 notbinot1 34183 elpadd0 35590 pm10.252 39054 pm10.253 39055 2exanali 39081 |
Copyright terms: Public domain | W3C validator |