![]() |
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 332 | 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 1107 3ianor 1108 hadnot 1604 cadnot 1617 2exanali 1864 nelb 3223 nsspssun 4218 undif3 4251 2nreu 4402 intirr 6073 ordtri3or 6350 nf1const 7251 nf1oconst 7252 frxp 8059 ressuppssdif 8117 suppofssd 8135 naddcllem 8623 domunfican 9265 ssfin4 10247 prinfzo0 13612 swrdnnn0nd 14545 swrdnd0 14546 lcmfunsnlem2lem1 16515 ncoprmlnprm 16604 prm23ge5 16688 smndex2dnrinv 18726 symgfix2 19199 gsumdixp 20034 cnfldfun 20811 symgmatr01lem 22005 ppttop 22360 zclmncvs 24515 mdegleb 25432 2lgslem3 26755 trlsegvdeg 29174 strlem1 31195 difrab2 31429 isarchi 32021 bnj1189 33624 dfacycgr1 33741 fmlasucdisj 33996 dfon3 34480 wl-3xornot 35955 poimirlem18 36099 poimirlem21 36102 poimirlem30 36111 poimirlem31 36112 ftc1anclem3 36156 hdmaplem4 40240 mapdh9a 40255 onsupmaxb 41576 dflim5 41666 faosnf0.11b 41706 ifpnot23 41757 ifpdfxor 41766 ifpnim1 41776 ifpnim2 41778 dfsucon 41802 ntrneineine1lem 42363 disjrnmpt2 43414 aiotavb 45329 dfatprc 45369 ndmafv2nrn 45461 nfunsnafv2 45464 oddneven 45843 |
Copyright terms: Public domain | W3C validator |