![]() |
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 3522 ceqsexv 3524 gencbval 3536 ceqsralbv 3643 snnzb 4720 raldifsnb 4797 uni0b 4935 opab0 5552 tsna1 36949 ralopabb 42094 |
Copyright terms: Public domain | W3C validator |