![]() |
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 153 | . 2 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | |
2 | con4 113 | . 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: mtt 364 pm4.14 807 dfbi3 1049 ifpdfbi 1070 r19.23v 3180 raldifsni 4799 dff14a 7289 weniso 7373 dfom2 7888 dfsup2 9481 wemapsolem 9587 pwfseqlem3 10697 indstr 12955 rpnnen2lem12 16257 algcvgblem 16610 isirred2 20437 isdomn2OLD 20728 isdomn3 20731 ist0-3 23368 mdegleb 26117 dchrelbas4 27301 toslublem 32946 tosglblem 32948 bj-alcomexcom 36662 poimirlem25 37631 poimirlem30 37636 tsbi3 38121 ntrneikb 44083 aacllem 49031 |
Copyright terms: Public domain | W3C validator |