![]() |
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 223 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 1, 3 | xchnxbi 331 | 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: 3ioran 1106 3ianor 1107 hadnot 1603 cadnot 1616 2exanali 1863 nelb 3222 nsspssun 4217 undif3 4250 2nreu 4401 intirr 6072 ordtri3or 6349 nf1const 7249 nf1oconst 7250 frxp 8057 ressuppssdif 8115 suppofssd 8133 naddcllem 8621 domunfican 9263 ssfin4 10245 prinfzo0 13610 swrdnnn0nd 14543 swrdnd0 14544 lcmfunsnlem2lem1 16513 ncoprmlnprm 16602 prm23ge5 16686 smndex2dnrinv 18724 symgfix2 19196 gsumdixp 20031 cnfldfun 20806 symgmatr01lem 22000 ppttop 22355 zclmncvs 24510 mdegleb 25427 2lgslem3 26750 trlsegvdeg 29169 strlem1 31190 difrab2 31424 isarchi 32013 bnj1189 33612 dfacycgr1 33729 fmlasucdisj 33984 dfon3 34468 wl-3xornot 35943 poimirlem18 36087 poimirlem21 36090 poimirlem30 36099 poimirlem31 36100 ftc1anclem3 36144 hdmaplem4 40228 mapdh9a 40243 onsupmaxb 41551 dflim5 41641 faosnf0.11b 41681 ifpnot23 41732 ifpdfxor 41741 ifpnim1 41751 ifpnim2 41753 dfsucon 41777 ntrneineine1lem 42338 disjrnmpt2 43383 aiotavb 45294 dfatprc 45334 ndmafv2nrn 45426 nfunsnafv2 45429 oddneven 45808 |
Copyright terms: Public domain | W3C validator |