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 318 notbi 319 2falsed 377 had0 1606 cbvexdvaw 2043 cbvexdw 2337 cbvexd 2409 rexeqbidvv 3340 vtoclgft 3493 sbcne12 4347 ordsucuniel 7680 rankr1a 9603 ltaddsub 11458 leaddsub 11460 supxrbnd1 13064 supxrbnd2 13065 ioo0 13113 ico0 13134 ioc0 13135 icc0 13136 fllt 13535 rabssnn0fi 13715 elcls 22233 rusgrnumwwlks 28348 chrelat3 30742 sltrec 34023 bj-equsexvwd 34972 wl-sb8et 35717 infxrbnd2 42915 oddprmne2 45178 nnolog2flm1 45947 |
Copyright terms: Public domain | W3C validator |