| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > xchbinxr | Structured version Visualization version GIF version | ||
| Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
| Ref | Expression |
|---|---|
| xchbinxr.1 | ⊢ (𝜑 ↔ ¬ 𝜓) |
| xchbinxr.2 | ⊢ (𝜒 ↔ 𝜓) |
| Ref | Expression |
|---|---|
| xchbinxr | ⊢ (𝜑 ↔ ¬ 𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xchbinxr.1 | . 2 ⊢ (𝜑 ↔ ¬ 𝜓) | |
| 2 | xchbinxr.2 | . . 3 ⊢ (𝜒 ↔ 𝜓) | |
| 3 | 2 | bicomi 224 | . 2 ⊢ (𝜓 ↔ 𝜒) |
| 4 | 1, 3 | xchbinx 334 | 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: con2bii 357 2nalexn 1828 2exnaln 1829 sbn 2280 ralnex 3072 rexanali 3102 r2exlem 3143 nelbOLD 3235 dfss6 3973 nss 4048 difdif 4135 indifdi 4294 difab 4310 neq0 4352 ssdif0 4366 difin0ss 4373 sbcnel12g 4414 disjsn 4711 iundif2 5074 iindif2 5077 brsymdif 5202 rexxfr 5416 nssss 5460 reldm0 5938 domtriord 9163 rnelfmlem 23960 dchrfi 27299 noinfbnd1lem4 27771 wwlksnext 29913 dff15 35098 df3nandALT2 36401 wl-3xornot1 37481 poimirlem1 37628 dvasin 37711 lcvbr3 39024 cvrval2 39275 hashnexinj 42129 wopprc 43042 onsucf1olem 43283 sqrtcvallem1 43644 gneispace 44147 iindif2f 45165 aiota0ndef 47109 isubgr3stgrlem3 47935 |
| Copyright terms: Public domain | W3C validator |