Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > con34b | Structured version Visualization version GIF version |
Description: A biconditional form of contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.) |
Ref | Expression |
---|---|
con34b | ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con3 148 | . 2 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | |
2 | con4 111 | . 2 ⊢ ((¬ 𝜓 → ¬ 𝜑) → (𝜑 → 𝜓)) | |
3 | 1, 2 | impbii 198 | 1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: mtt 353 pm4.14 600 19.23t 2066 19.23tOLD 2206 r19.23v 3005 raldifsni 4265 dff14a 6427 weniso 6504 dfom2 6959 dfsup2 8233 wemapsolem 8338 pwfseqlem3 9361 indstr 11632 rpnnen2lem12 14793 algcvgblem 15128 isirred2 18524 isdomn2 19120 ist0-3 20959 mdegleb 23628 dchrelbas4 24768 toslublem 28998 tosglblem 29000 poimirlem25 32604 poimirlem30 32609 tsbi3 33112 isdomn3 36801 ntrneikb 37412 conss34OLD 37667 aacllem 42356 |
Copyright terms: Public domain | W3C validator |