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 316 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | con1bii.1 | . . 3 ⊢ (¬ 𝜑 ↔ 𝜓) | |
3 | 1, 2 | xchbinx 335 | . 2 ⊢ (𝜑 ↔ ¬ 𝜓) |
4 | 3 | bicomi 225 | 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: xor 1008 3anor 1100 3oran 1101 2nexaln 1821 2exanali 1851 nnel 3129 spc2d 3600 npss 4084 dfnul3 4292 snprc 4645 dffv2 6749 kmlem3 9566 axpowndlem3 10009 nnunb 11881 rpnnen2lem12 15566 dsmmacl 20813 ntreq0 21613 largei 29971 ballotlem2 31645 dffr5 32886 noetalem3 33116 brsset 33247 brtxpsd 33252 dfrecs2 33308 dfint3 33310 con1bii2 34495 notbinot1 35238 elpadd0 36825 pm10.252 40570 pm10.253 40571 |
Copyright terms: Public domain | W3C validator |