![]() |
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 315 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | con1bii.1 | . . 3 ⊢ (¬ 𝜑 ↔ 𝜓) | |
3 | 1, 2 | xchbinx 334 | . 2 ⊢ (𝜑 ↔ ¬ 𝜓) |
4 | 3 | bicomi 223 | 1 ⊢ (¬ 𝜓 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 |
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 |
This theorem is referenced by: xor 1014 3anor 1109 3oran 1110 2nexaln 1833 2exanali 1864 nnel 3057 spc2d 3560 npss 4069 dfnul3OLD 4287 snprc 4677 dffv2 6932 kmlem3 10022 axpowndlem3 10469 nnunb 12343 rpnnen2lem12 16043 dsmmacl 21076 ntreq0 22356 noetasuplem4 27012 noetainflem4 27016 largei 31014 ballotlem2 32868 dffr5 34121 brsset 34405 brtxpsd 34410 dfrecs2 34466 dfint3 34468 con1bii2 35734 notbinot1 36469 elpadd0 38203 pm10.252 42442 pm10.253 42443 ralfal 43177 |
Copyright terms: Public domain | W3C validator |