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 224 | . . 3 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓)) |
3 | 2 | con2bid 356 | . 2 ⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒)) |
4 | 3 | bicomd 224 | 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: pm5.18 383 necon1bbid 3052 r19.9rzv 4441 onmindif 6273 iotanul 6326 ondif2 8116 cnpart 14587 sadadd2lem2 15787 isnirred 19379 isreg2 21913 kqcldsat 22269 trufil 22446 itg2cnlem2 24290 issqf 25640 eupth2lem3lem4 27937 pjnorm2 29431 atdmd 30102 atmd2 30104 dfrdg4 33309 dalawlem13 36899 infordmin 39777 |
Copyright terms: Public domain | W3C validator |