![]() |
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 953 3anor 1075 3oran 1077 2nexaln 1797 nnel 2935 npss 3750 symdifass 3886 dfnul3 3951 snprc 4285 dffv2 6310 kmlem3 9012 axpowndlem3 9459 nnunb 11326 rpnnen2lem12 14998 dsmmacl 20133 ntreq0 20929 largei 29254 spc2d 29441 ballotlem2 30678 dffr5 31769 noetalem3 31990 brsset 32121 brtxpsd 32126 dfrecs2 32182 dfint3 32184 con1bii2 33309 notbinot1 34008 elpadd0 35413 pm10.252 38877 pm10.253 38878 2exanali 38904 |
Copyright terms: Public domain | W3C validator |