![]() |
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 1072 2nalexn 1795 2exnaln 1796 sbn 2419 ralnex 3021 ralnexOLD 3022 rexanali 3027 r2exlem 3088 dfss6 3626 nss 3696 difdif 3769 difab 3929 ssdif0 3975 difin0ss 3979 sbcnel12g 4018 disjsn 4278 iundif2 4619 iindif2 4621 brsymdif 4744 notzfaus 4870 rexxfr 4918 nssss 4954 reldm0 5375 domtriord 8147 rnelfmlem 21803 dchrfi 25025 wwlksnext 26856 df3nandALT2 32522 bj-ssbn 32766 poimirlem1 33540 dvasin 33626 lcvbr3 34628 cvrval2 34879 wopprc 37914 gneispace 38749 |
Copyright terms: Public domain | W3C validator |