| 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 320 | . 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒) |
| 4 | 1, 3 | bitri 275 | 1 ⊢ (𝜑 ↔ ¬ 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: xchbinxr 335 con1bii 356 anor 985 pm4.52 987 pm4.54 989 xordi 1019 xorcom 1514 xorneg1 1522 xorbi12i 1524 norcom 1530 nornot 1531 noran 1532 trunanfal 1582 truxortru 1585 truxorfal 1586 falxorfal 1588 trunortru 1589 trunorfal 1590 falnorfal 1592 nic-mpALT 1672 nic-axALT 1674 sbex 2281 necon3abii 2987 ne3anior 3036 rexab 3700 inssdif0 4374 falseral0 4516 dtruALT 5388 dm0rn0 5935 brprcneu 6896 brprcneuALT 6897 soseq 8184 0nelfz1 13583 pmltpc 25485 cofcutr 27958 nbgrnself 29376 rgrx0ndm 29611 clwwlkneq0 30048 nfrgr2v 30291 frgrncvvdeqlem1 30318 cvbr2 32302 bnj1143 34804 fmlan0 35396 brsset 35890 brtxpsd 35895 dffun10 35915 dfint3 35953 brub 35955 wl-nfeqfb 37537 sbcni 38118 brvdif2 38263 dfssr2 38500 lcvbr2 39023 atlrelat1 39322 dfxor5 43780 df3an2 43782 clsk1independent 44059 spr0nelg 47463 341fppr2 47721 9fppr8 47724 pgrpgt2nabl 48282 lmod1zrnlvec 48411 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |