![]() |
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 223 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | xchbinx 333 | 1 ⊢ (𝜑 ↔ ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 |
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 206 |
This theorem is referenced by: con2bii 356 2nalexn 1822 2exnaln 1823 sbn 2269 ralnex 3069 rexanali 3099 r2exlem 3140 nelbOLD 3230 dfss6 3971 nss 4046 difdif 4131 indifdi 4286 difab 4303 neq0 4349 ssdif0 4367 difin0ss 4372 sbcnel12g 4415 disjsn 4720 iundif2 5081 iindif2 5084 brsymdif 5211 rexxfr 5420 nssss 5461 reldm0 5934 domtriord 9154 rnelfmlem 23876 dchrfi 27208 noinfbnd1lem4 27679 wwlksnext 29724 dff15 34740 df3nandALT2 35917 wl-3xornot1 36992 poimirlem1 37127 dvasin 37210 lcvbr3 38527 cvrval2 38778 hashnexinj 41631 wopprc 42482 onsucf1olem 42730 sqrtcvallem1 43092 gneispace 43595 iindif2f 44561 aiota0ndef 46506 |
Copyright terms: Public domain | W3C validator |