![]() |
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 214 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | xchbinx 323 | 1 ⊢ (𝜑 ↔ ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 |
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 197 |
This theorem is referenced by: 3anorOLD 1094 2nalexn 1892 2exnaln 1893 sbn 2516 ralnex 3118 ralnexOLD 3119 rexanali 3124 r2exlem 3185 dfss6 3722 nss 3792 difdif 3867 difab 4027 ssdif0 4073 difin0ss 4077 sbcnel12g 4116 disjsn 4378 iundif2 4727 iindif2 4729 brsymdif 4851 notzfaus 4977 rexxfr 5025 nssss 5061 reldm0 5486 domtriord 8259 rnelfmlem 21928 dchrfi 25150 wwlksnext 26982 df3nandALT2 32674 bj-ssbn 32918 poimirlem1 33692 dvasin 33778 lcvbr3 34782 cvrval2 35033 wopprc 38068 gneispace 38903 |
Copyright terms: Public domain | W3C validator |