![]() |
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 352 | . 2 ⊢ ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒)) | |
3 | 1, 2 | sylibr 233 | 1 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: con1bid 354 sotric 5621 sotrieq 5622 sotr2 5625 isso2i 5628 sotr3 5632 sotri2 6140 sotri3 6141 somin1 6144 somincom 6145 ordtri2 6410 ordtr3 6420 ordintdif 6425 ord0eln0 6430 soisoi 7339 weniso 7365 ordunisuc2 7853 limsssuc 7859 nlimon 7860 tfrlem15 8421 oawordeulem 8583 nnawordex 8666 onomeneqOLD 9266 fimaxg 9327 suplub2 9500 fiming 9537 wemapsolem 9589 cantnflem1 9728 rankval3b 9865 cardsdomel 10013 harsdom 10034 isfin1-2 10424 fin1a2lem7 10445 suplem2pr 11092 xrltnle 11327 ltnle 11339 leloe 11346 xrlttri 13167 xrleloe 13172 xrrebnd 13196 supxrbnd2 13350 supxrbnd 13356 om2uzf1oi 13968 rabssnn0fi 14001 cnpart 15240 bits0e 16424 bitsmod 16431 bitsinv1lem 16436 sadcaddlem 16452 trfil2 23874 xrsxmet 24808 metdsge 24848 ovolunlem1a 25508 ovolunlem1 25509 itg2seq 25755 noetasuplem4 27758 noetainflem4 27762 sltnle 27775 sleloe 27776 toslublem 32830 tosglblem 32832 isarchi2 33027 gsumesum 33848 sgnneg 34330 elfuns 35687 finminlem 35978 bj-bibibi 36239 itg2addnclem 37320 heiborlem10 37469 aks4d1p8 41734 cantnfresb 42927 naddwordnexlem4 43005 ontric3g 43126 or3or 43627 ntrclselnel2 43662 clsneifv3 43714 islininds2 47804 |
Copyright terms: Public domain | W3C validator |