![]() |
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 249 | . . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | con4d 115 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1 | biimpd 230 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) |
5 | 3, 4 | impcon4bid 228 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: notbid 319 notbi 320 had0 1590 cbvexd 2387 cbvrexdva2OLD 3411 vtoclgft 3499 sbcne12 4290 ordsucuniel 7402 rankr1a 9118 ltaddsub 10968 leaddsub 10970 supxrbnd1 12568 supxrbnd2 12569 ioo0 12617 ico0 12638 ioc0 12639 icc0 12640 fllt 13030 rabssnn0fi 13208 elcls 21369 rusgrnumwwlks 27439 chrelat3 29835 sltrec 32889 wl-sb8et 34341 infxrbnd2 41199 oddprmne2 43384 nnolog2flm1 44153 |
Copyright terms: Public domain | W3C validator |