![]() |
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 355 | . 2 ⊢ ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒)) | |
3 | 1, 2 | sylibr 235 | 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: con1bid 357 sotric 5381 sotrieq 5382 sotr2 5385 isso2i 5388 sotri2 5857 sotri3 5858 somin1 5861 somincom 5862 ordtri2 6093 ordtr3 6103 ordintdif 6107 ord0eln0 6112 soisoi 6935 weniso 6961 ordunisuc2 7406 limsssuc 7412 nlimon 7413 tfrlem15 7871 oawordeulem 8021 nnawordex 8104 onomeneq 8544 fimaxg 8601 suplub2 8761 fiming 8798 wemapsolem 8850 cantnflem1 8987 rankval3b 9090 cardsdomel 9238 harsdom 9259 isfin1-2 9642 fin1a2lem7 9663 suplem2pr 10310 xrltnle 10544 ltnle 10556 leloe 10563 xrlttri 12371 xrleloe 12376 xrrebnd 12400 supxrbnd2 12554 supxrbnd 12560 om2uzf1oi 13159 rabssnn0fi 13192 cnpart 14421 bits0e 15599 bitsmod 15606 bitsinv1lem 15611 sadcaddlem 15627 trfil2 22167 xrsxmet 23088 metdsge 23128 ovolunlem1a 23768 ovolunlem1 23769 itg2seq 24014 toslublem 30298 tosglblem 30300 isarchi2 30410 gsumesum 30891 sgnneg 31371 sotr3 32555 noetalem3 32773 sltnle 32786 sleloe 32787 elfuns 32930 finminlem 33220 bj-bibibi 33470 itg2addnclem 34420 heiborlem10 34576 ontric3g 39324 or3or 39807 ntrclselnel2 39844 clsneifv3 39896 islininds2 43973 |
Copyright terms: Public domain | W3C validator |