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 226 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | xchbinx 336 | 1 ⊢ (𝜑 ↔ ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 208 |
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 209 |
This theorem is referenced by: con2bii 360 2nalexn 1824 2exnaln 1825 sbn 2283 sbnOLD 2537 sbnALT 2591 ralnex 3236 rexanali 3265 nelb 3268 r2exlem 3302 dfss6 3956 nss 4028 difdif 4106 difab 4271 ssdif0 4322 difin0ss 4327 sbcnel12g 4362 disjsn 4640 iundif2 4988 iindif2 4991 brsymdif 5117 notzfausOLD 5255 rexxfr 5308 nssss 5340 reldm0 5792 domtriord 8657 rnelfmlem 22554 dchrfi 25825 wwlksnext 27665 dff15 32348 df3nandALT2 33743 poimirlem1 34887 dvasin 34972 lcvbr3 36153 cvrval2 36404 wopprc 39620 gneispace 40477 aiota0ndef 43289 |
Copyright terms: Public domain | W3C validator |