| 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 1050 ifpdfbi 1071 r19.23v 3183 raldifsni 4795 dff14a 7290 weniso 7374 dfom2 7889 dfsup2 9484 wemapsolem 9590 pwfseqlem3 10700 indstr 12958 rpnnen2lem12 16261 algcvgblem 16614 isirred2 20421 isdomn2OLD 20712 isdomn3 20715 ist0-3 23353 mdegleb 26103 dchrelbas4 27287 toslublem 32962 tosglblem 32964 bj-alcomexcom 36681 poimirlem25 37652 poimirlem30 37657 tsbi3 38142 ntrneikb 44107 fulltermc 49143 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |