![]() |
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 2398 cbvex2 2411 2ralorOLD 3221 rexcom 3274 cbvrexfw 3289 ceqsex 3493 ceqsexv 3495 gencbval 3507 ceqsralbv 3608 snnzb 4680 raldifsnb 4757 uni0b 4895 opab0 5512 tsna1 36606 ralopabb 41690 |
Copyright terms: Public domain | W3C validator |