![]() |
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 238 | . . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | con4d 114 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1 | biimpd 219 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) |
5 | 3, 4 | impcon4bid 217 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: notbid 307 notbi 308 had0 1583 cbvexdva 2319 sbcne12 4019 ordsucuniel 7066 rankr1a 8737 ltaddsub 10540 leaddsub 10542 supxrbnd1 12189 supxrbnd2 12190 ioo0 12238 ico0 12259 ioc0 12260 icc0 12261 fllt 12647 rabssnn0fi 12825 elcls 20925 rusgrnumwwlks 26941 chrelat3 29358 sltrec 32049 wl-sb8et 33464 infxrbnd2 39898 oddprmne2 41949 nnolog2flm1 42709 |
Copyright terms: Public domain | W3C validator |