![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con1bid | Structured version Visualization version GIF version |
Description: A contraposition deduction. (Contributed by NM, 9-Oct-1999.) |
Ref | Expression |
---|---|
con1bid.1 | ⊢ (𝜑 → (¬ 𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
con1bid | ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con1bid.1 | . . . 4 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝜒)) | |
2 | 1 | bicomd 223 | . . 3 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓)) |
3 | 2 | con2bid 354 | . 2 ⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒)) |
4 | 3 | bicomd 223 | 1 ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 |
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 207 |
This theorem is referenced by: pm5.18 381 necon1bbid 2978 r19.9rzv 4506 rexsng 4681 onmindif 6478 iotanul 6541 ondif2 8539 cnpart 15276 sadadd2lem2 16484 isnirred 20437 isreg2 23401 kqcldsat 23757 trufil 23934 itg2cnlem2 25812 issqf 27194 eupth2lem3lem4 30260 pjnorm2 31756 atdmd 32427 atmd2 32429 dfrdg4 35933 dalawlem13 39866 sticksstones1 42128 aks6d1c6lem4 42155 orddif0suc 43258 infordmin 43522 |
Copyright terms: Public domain | W3C validator |