![]() |
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 216 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | xchbinx 326 | 1 ⊢ (𝜑 ↔ ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 |
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 199 |
This theorem is referenced by: 2nalexn 1871 2exnaln 1872 sbn 2467 ralnex 3174 rexanali 3179 r2exlem 3244 dfss6 3811 nss 3882 difdif 3959 difab 4122 ssdif0 4172 difin0ss 4177 sbcnel12g 4210 disjsn 4478 iundif2 4822 iindif2 4824 brsymdif 4947 notzfaus 5076 rexxfr 5130 nssss 5158 reldm0 5590 domtriord 8396 rnelfmlem 22175 dchrfi 25443 wwlksnext 27271 df3nandALT2 32991 bj-ssbn 33239 poimirlem1 34045 dvasin 34130 lcvbr3 35186 cvrval2 35437 wopprc 38570 gneispace 39402 aiota0ndef 42139 |
Copyright terms: Public domain | W3C validator |