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 137. (Contributed by NM, 12-Mar-1993.) |
Ref | Expression |
---|---|
con2b | ⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con2 137 | . 2 ⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑)) | |
2 | con2 137 | . 2 ⊢ ((𝜓 → ¬ 𝜑) → (𝜑 → ¬ 𝜓)) | |
3 | 1, 2 | impbii 210 | 1 ⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: mt2bi 365 pm4.15 828 nancom 1480 nic-ax 1665 nic-axALT 1666 alimex 1822 dfdif3 4088 ssconb 4111 disjsn 4639 oneqmini 6235 kmlem4 9567 isprm3 16015 bnj1171 32169 bnj1176 32174 bnj1204 32181 bnj1388 32202 bnj1523 32240 fvineqsneq 34575 dfxor5 39990 pm13.196a 40623 |
Copyright terms: Public domain | W3C validator |