![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xchbinx | Structured version Visualization version GIF version |
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
Ref | Expression |
---|---|
xchbinx.1 | ⊢ (𝜑 ↔ ¬ 𝜓) |
xchbinx.2 | ⊢ (𝜓 ↔ 𝜒) |
Ref | Expression |
---|---|
xchbinx | ⊢ (𝜑 ↔ ¬ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xchbinx.1 | . 2 ⊢ (𝜑 ↔ ¬ 𝜓) | |
2 | xchbinx.2 | . . 3 ⊢ (𝜓 ↔ 𝜒) | |
3 | 2 | notbii 319 | . 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒) |
4 | 1, 3 | bitri 274 | 1 ⊢ (𝜑 ↔ ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ 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: xchbinxr 334 con1bii 355 anor 980 pm4.52 982 pm4.54 984 xordi 1014 xorcom 1507 xorneg1 1515 xorbi12i 1517 norcom 1523 nornot 1524 noran 1525 trunanfal 1575 truxortru 1578 truxorfal 1579 falxorfal 1581 trunortru 1582 trunorfal 1583 falnorfal 1585 nic-mpALT 1666 nic-axALT 1668 sbex 2270 necon3abii 2976 ne3anior 3025 rexab 3686 inssdif0 4371 falseral0 4521 dtruALT 5388 dm0rn0 5927 brprcneu 6886 brprcneuALT 6887 soseq 8164 0nelfz1 13555 pmltpc 25423 cofcutr 27890 nbgrnself 29244 rgrx0ndm 29479 clwwlkneq0 29911 nfrgr2v 30154 frgrncvvdeqlem1 30181 cvbr2 32165 bnj1143 34549 fmlan0 35129 brsset 35613 brtxpsd 35618 dffun10 35638 dfint3 35676 brub 35678 wl-nfeqfb 37131 sbcni 37712 brvdif2 37861 dfssr2 38098 lcvbr2 38621 atlrelat1 38920 dfxor5 43336 df3an2 43338 clsk1independent 43615 spr0nelg 46950 341fppr2 47208 9fppr8 47211 pgrpgt2nabl 47613 lmod1zrnlvec 47745 aacllem 48417 |
Copyright terms: Public domain | W3C validator |