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 156 | . 2 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | |
2 | con4 113 | . 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: mtt 366 pm4.14 803 dfbi3 1041 r19.23v 3276 raldifsni 4720 dff14a 7019 weniso 7096 dfom2 7571 dfsup2 8896 wemapsolem 9002 pwfseqlem3 10070 indstr 12304 rpnnen2lem12 15566 algcvgblem 15909 isirred2 19380 isdomn2 20000 ist0-3 21881 mdegleb 24585 dchrelbas4 25746 toslublem 30581 tosglblem 30583 poimirlem25 34798 poimirlem30 34803 tsbi3 35294 isdomn3 39682 ntrneikb 40322 aacllem 44830 |
Copyright terms: Public domain | W3C validator |