| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > con2b | Structured version Visualization version GIF version | ||
| Description: Contraposition. Bidirectional version of con2 135. (Contributed by NM, 12-Mar-1993.) |
| Ref | Expression |
|---|---|
| con2b | ⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con2 135 | . 2 ⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑)) | |
| 2 | con2 135 | . 2 ⊢ ((𝜓 → ¬ 𝜑) → (𝜑 → ¬ 𝜓)) | |
| 3 | 1, 2 | impbii 209 | 1 ⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: mt2bi 363 pm4.15 833 nancom 1496 nic-ax 1673 nic-axALT 1674 alimex 1831 dfdif3OLD 4118 ssconb 4142 disjsn 4711 oneqmini 6436 kmlem4 10194 isprm3 16720 ssdifidlprm 33486 bnj1171 35014 bnj1176 35019 bnj1204 35026 bnj1388 35047 bnj1523 35085 fvineqsneq 37413 dfxor5 43780 pm13.196a 44433 sswfaxreg 45004 |
| Copyright terms: Public domain | W3C validator |