![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con4bii | Structured version Visualization version GIF version |
Description: A contraposition inference. (Contributed by NM, 21-May-1994.) |
Ref | Expression |
---|---|
con4bii.1 | ⊢ (¬ 𝜑 ↔ ¬ 𝜓) |
Ref | Expression |
---|---|
con4bii | ⊢ (𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con4bii.1 | . 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓) | |
2 | notbi 319 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓)) | |
3 | 1, 2 | mpbir 230 | 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: 2false 376 equsexvw 2009 cbvexv1 2339 cbvex2v 2341 cbvex 2399 cbvex2 2412 2ralorOLD 3230 rexcom 3288 cbvrexfw 3303 ceqsex 3524 ceqsexv 3526 gencbval 3538 ceqsralbv 3646 snnzb 4723 raldifsnb 4800 uni0b 4938 opab0 5555 tsna1 37060 ralopabb 42210 |
Copyright terms: Public domain | W3C validator |