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 251 | . . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | con4d 115 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1 | biimpd 232 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) |
5 | 3, 4 | impcon4bid 230 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 |
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 210 |
This theorem is referenced by: notbid 321 notbi 322 2falsed 380 had0 1610 cbvexdvaw 2051 cbvexdw 2342 cbvexd 2409 rexeqbidvv 3308 vtoclgft 3460 sbcne12 4312 ordsucuniel 7570 rankr1a 9350 ltaddsub 11204 leaddsub 11206 supxrbnd1 12809 supxrbnd2 12810 ioo0 12858 ico0 12879 ioc0 12880 icc0 12881 fllt 13279 rabssnn0fi 13457 elcls 21836 rusgrnumwwlks 27924 chrelat3 30318 sltrec 33669 bj-equsexvwd 34618 wl-sb8et 35363 infxrbnd2 42486 oddprmne2 44748 nnolog2flm1 45517 |
Copyright terms: Public domain | W3C validator |