![]() |
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 376 had0 1605 cbvexdvaw 2042 cbvexdw 2335 cbvexd 2406 cbvrexdva 3236 raleq 3321 rexeqbidvvOLD 3331 cbvrexdva2 3344 rexeqf 3349 vtoclgft 3537 sbcne12 4408 ordsucuniel 7795 rankr1a 9813 ltaddsub 11670 leaddsub 11672 supxrbnd1 13282 supxrbnd2 13283 ioo0 13331 ico0 13352 ioc0 13353 icc0 13354 fllt 13753 rabssnn0fi 13933 elcls 22506 sltrec 27247 rusgrnumwwlks 29093 chrelat3 31487 bj-equsexvwd 35463 wl-sb8et 36222 wl-issetft 36248 infxrbnd2 43852 oddprmne2 46155 nnolog2flm1 46924 |
Copyright terms: Public domain | W3C validator |