![]() |
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 247 | . . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | con4d 115 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1 | biimpd 228 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) |
5 | 3, 4 | impcon4bid 226 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: notbid 317 notbi 318 2falsed 375 had0 1598 cbvexdvaw 2035 cbvexdw 2330 cbvexd 2402 cbvrexdva 3228 raleq 3312 rexeqbidvvOLD 3322 cbvrexdva2 3333 rexeqf 3338 issetft 3477 sbcne12 4417 ordsucuniel 7833 rankr1a 9879 ltaddsub 11738 leaddsub 11740 supxrbnd1 13354 supxrbnd2 13355 ioo0 13403 ico0 13424 ioc0 13425 icc0 13426 fllt 13826 rabssnn0fi 14006 elcls 23068 sltrec 27850 rusgrnumwwlks 29908 chrelat3 32304 bj-equsexvwd 36486 wl-sb8eft 37246 wl-sb8et 37248 wl-issetft 37277 infxrbnd2 44984 oddprmne2 47287 nnolog2flm1 47978 |
Copyright terms: Public domain | W3C validator |