![]() |
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 312 | . 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒) |
4 | 1, 3 | bitri 267 | 1 ⊢ (𝜑 ↔ ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 |
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 199 |
This theorem is referenced by: xchbinxr 327 con1bii 348 pm4.52 1014 pm4.54 1016 xordi 1047 3anorOLD 1136 nancomOLD 1620 nannotOLD 1625 xorneg1 1650 trunanfal 1701 truxortru 1704 truxorfal 1705 falxorfal 1707 nic-mpALT 1773 nic-axALT 1775 sbanv 2340 sban 2530 sbex 2597 necon3abii 3045 ne3anior 3092 ralnex2 3255 ralnex3 3256 inssdif0 4177 falseral0 4301 dtruALT 5087 dtruALT2 5132 dm0rn0 5574 brprcneu 6425 0nelfz1 12653 pmltpc 23616 nbgrnself 26656 rgrx0ndm 26891 clwwlkneq0 27371 nfrgr2v 27653 frgrncvvdeqlem1 27680 cvbr2 29697 bnj1143 31407 soseq 32293 brsset 32535 brtxpsd 32540 dffun10 32560 dfint3 32598 brub 32600 wl-nfeqfb 33867 sbcni 34455 brvdif2 34580 dfssr2 34797 lcvbr2 35097 atlrelat1 35396 dfxor5 38900 df3an2 38902 clsk1independent 39184 spr0nelg 42573 pgrpgt2nabl 42994 lmod1zrnlvec 43130 aacllem 43443 |
Copyright terms: Public domain | W3C validator |