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 227 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 1, 3 | xchnxbi 335 | 1 ⊢ (¬ 𝜒 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 |
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 210 |
This theorem is referenced by: 3ioran 1108 3ianor 1109 hadnot 1609 cadnot 1622 2exanali 1868 nsspssun 4172 undif3 4205 2nreu 4356 intirr 5983 ordtri3or 6245 nf1const 7114 nf1oconst 7115 frxp 7893 ressuppssdif 7927 suppofssd 7945 domunfican 8944 ssfin4 9924 prinfzo0 13281 swrdnnn0nd 14221 swrdnd0 14222 lcmfunsnlem2lem1 16195 ncoprmlnprm 16284 prm23ge5 16368 smndex2dnrinv 18342 symgfix2 18808 gsumdixp 19627 cnfldfunALT 20376 symgmatr01lem 21550 ppttop 21904 zclmncvs 24045 mdegleb 24962 2lgslem3 26285 trlsegvdeg 28310 strlem1 30331 difrab2 30564 isarchi 31155 bnj1189 32702 dfacycgr1 32819 fmlasucdisj 33074 xpord3pred 33535 naddcllem 33568 dfon3 33931 wl-3xornot 35389 poimirlem18 35532 poimirlem21 35535 poimirlem30 35544 poimirlem31 35545 ftc1anclem3 35589 hdmaplem4 39525 mapdh9a 39540 ifpnot23 40770 ifpdfxor 40779 ifpnim1 40789 ifpnim2 40791 dfsucon 40815 ntrneineine1lem 41371 disjrnmpt2 42399 aiotavb 44254 dfatprc 44294 ndmafv2nrn 44386 nfunsnafv2 44389 oddneven 44769 |
Copyright terms: Public domain | W3C validator |