Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xchnxbir | Structured version Visualization version GIF version |
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
Ref | Expression |
---|---|
xchnxbir.1 | ⊢ (¬ 𝜑 ↔ 𝜓) |
xchnxbir.2 | ⊢ (𝜒 ↔ 𝜑) |
Ref | Expression |
---|---|
xchnxbir | ⊢ (¬ 𝜒 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xchnxbir.1 | . 2 ⊢ (¬ 𝜑 ↔ 𝜓) | |
2 | xchnxbir.2 | . . 3 ⊢ (𝜒 ↔ 𝜑) | |
3 | 2 | bicomi 214 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 1, 3 | xchnxbi 322 | 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: 3ioran 1056 hadnot 1541 cadnot 1554 nsspssun 3857 undif3 3888 undif3OLD 3889 intirr 5514 ordtri3or 5755 frxp 7287 ressuppssdif 7316 domunfican 8233 ssfin4 9132 prinfzo0 12506 lcmfunsnlem2lem1 15351 ncoprmlnprm 15436 prm23ge5 15520 symgfix2 17836 gsumdixp 18609 cnfldfunALT 19759 symgmatr01lem 20459 ppttop 20811 zclmncvs 22948 mdegleb 23824 2lgslem3 25129 trlsegvdeg 27087 strlem1 29109 isarchi 29736 bnj1189 31077 dfon3 31999 poimirlem18 33427 poimirlem21 33430 poimirlem30 33439 poimirlem31 33440 ftc1anclem3 33487 hdmaplem4 37063 mapdh9a 37079 ifpnot23 37823 ifpdfxor 37832 ifpnim1 37842 ifpnim2 37844 relintabex 37887 ntrneineine1lem 38382 2exanali 38587 oddneven 41557 |
Copyright terms: Public domain | W3C validator |