Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > con2bid | Structured version Visualization version GIF version |
Description: A contraposition deduction. (Contributed by NM, 15-Apr-1995.) |
Ref | Expression |
---|---|
con2bid.1 | ⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒)) |
Ref | Expression |
---|---|
con2bid | ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con2bid.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒)) | |
2 | con2bi 343 | . 2 ⊢ ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒)) | |
3 | 1, 2 | sylibr 224 | 1 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: con1bid 345 sotric 5061 sotrieq 5062 sotr2 5064 isso2i 5067 sotri2 5525 sotri3 5526 somin1 5529 somincom 5530 ordtri2 5758 ordtr3 5769 ordintdif 5774 ord0eln0 5779 soisoi 6578 weniso 6604 ordunisuc2 7044 limsssuc 7050 nlimon 7051 tfrlem15 7488 oawordeulem 7634 nnawordex 7717 onomeneq 8150 fimaxg 8207 suplub2 8367 fiming 8404 wemapsolem 8455 cantnflem1 8586 rankval3b 8689 cardsdomel 8800 harsdom 8821 isfin1-2 9207 fin1a2lem7 9228 suplem2pr 9875 xrltnle 10105 ltnle 10117 leloe 10124 xrlttri 11972 xrleloe 11977 xrrebnd 11999 supxrbnd2 12152 supxrbnd 12158 om2uzf1oi 12752 rabssnn0fi 12785 cnpart 13980 bits0e 15151 bitsmod 15158 bitsinv1lem 15163 sadcaddlem 15179 trfil2 21691 xrsxmet 22612 metdsge 22652 ovolunlem1a 23264 ovolunlem1 23265 itg2seq 23509 toslublem 29667 tosglblem 29669 isarchi2 29739 gsumesum 30121 sgnneg 30602 sotr3 31656 noetalem3 31865 sltnle 31878 sleloe 31879 elfuns 32022 finminlem 32312 bj-bibibi 32571 itg2addnclem 33461 heiborlem10 33619 19.9alt 34252 or3or 38319 ntrclselnel2 38356 clsneifv3 38408 islininds2 42273 |
Copyright terms: Public domain | W3C validator |