|   | 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 2979 r19.9rzv 4499 rexsng 4675 onmindif 6475 iotanul 6538 ondif2 8541 cnpart 15280 sadadd2lem2 16488 isnirred 20421 isreg2 23386 kqcldsat 23742 trufil 23919 itg2cnlem2 25798 issqf 27180 eupth2lem3lem4 30251 pjnorm2 31747 atdmd 32418 atmd2 32420 dfrdg4 35953 dalawlem13 39886 sticksstones1 42148 aks6d1c6lem4 42175 orddif0suc 43286 infordmin 43550 | 
| Copyright terms: Public domain | W3C validator |