| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > con4bid | Structured version Visualization version GIF version | ||
| Description: A contraposition deduction. (Contributed by NM, 21-May-1994.) |
| Ref | Expression |
|---|---|
| con4bid.1 | ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
| Ref | Expression |
|---|---|
| con4bid | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con4bid.1 | . . . 4 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) | |
| 2 | 1 | biimprd 248 | . . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
| 3 | 2 | con4d 115 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 4 | 1 | biimpd 229 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) |
| 5 | 3, 4 | impcon4bid 227 | 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: notbid 318 notbi 319 2falsed 376 had0 1604 cbvexdvaw 2038 cbvexdw 2341 cbvexd 2413 cbvrexdva 3240 raleq 3323 rexeqbidvvOLD 3337 cbvrexdva2 3349 rexeqf 3354 cbvexeqsetf 3495 sbcne12 4415 ordsucuniel 7844 rankr1a 9876 ltaddsub 11737 leaddsub 11739 supxrbnd1 13363 supxrbnd2 13364 ioo0 13412 ico0 13433 ioc0 13434 icc0 13435 fllt 13846 rabssnn0fi 14027 elcls 23081 sltrec 27865 rusgrnumwwlks 29994 chrelat3 32390 bj-equsexvwd 36782 wl-sb8eft 37552 wl-sb8et 37554 wl-issetft 37583 infxrbnd2 45380 oddprmne2 47702 nnolog2flm1 48511 |
| Copyright terms: Public domain | W3C validator |