![]() |
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 309 | . 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒) |
4 | 1, 3 | bitri 264 | 1 ⊢ (𝜑 ↔ ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 |
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 197 |
This theorem is referenced by: xchbinxr 324 con1bii 345 pm4.52 969 pm4.54 971 xordi 1002 3anorOLD 1094 nancom 1598 nannot 1601 xorneg1 1623 trunanfal 1673 truxortru 1676 truxorfal 1677 falxorfal 1679 nic-mpALT 1745 nic-axALT 1747 sban 2546 sbex 2611 necon3abii 2989 ne3anior 3036 ralnex2 3193 ralnex3 3194 inssdif0 4094 falseral0 4220 dtruALT 5027 dtruALT2 5039 dm0rn0 5480 brprcneu 6325 0nelfz1 12567 pmltpc 23438 nbgrnself 26478 rgrx0ndm 26724 clwwlkneq0 27183 nfrgr2v 27454 frgrncvvdeqlem1 27481 cvbr2 29482 bnj1143 31199 soseq 32091 brsset 32333 brtxpsd 32338 dffun10 32358 dfint3 32396 brub 32398 wl-nfeqfb 33658 sbcni 34246 brvdif2 34369 dfssr2 34591 lcvbr2 34831 atlrelat1 35130 dfxor5 38585 df3an2 38587 clsk1independent 38870 spr0nelg 42254 pgrpgt2nabl 42675 lmod1zrnlvec 42811 aacllem 43078 |
Copyright terms: Public domain | W3C validator |