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 227 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | xchbinx 337 | 1 ⊢ (𝜑 ↔ ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 |
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 210 |
This theorem is referenced by: con2bii 361 2nalexn 1835 2exnaln 1836 sbn 2282 ralnex 3162 rexanali 3190 nelbOLD 3194 r2exlem 3229 dfss6 3903 nss 3977 difdif 4059 indifdi 4212 difab 4229 neq0 4274 ssdif0 4292 difin0ss 4297 sbcnel12g 4340 disjsn 4641 iundif2 4996 iindif2 4999 brsymdif 5126 notzfausOLD 5269 rexxfr 5323 nssss 5354 reldm0 5811 domtriord 8814 rnelfmlem 22873 dchrfi 26160 wwlksnext 28001 dff15 32792 noinfbnd1lem4 33692 df3nandALT2 34352 wl-3xornot1 35414 poimirlem1 35541 dvasin 35624 lcvbr3 36800 cvrval2 37051 wopprc 40583 sqrtcvallem1 40943 gneispace 41449 aiota0ndef 44289 |
Copyright terms: Public domain | W3C validator |