|   | 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 224 | . 2 ⊢ (𝜑 ↔ 𝜒) | 
| 4 | 1, 3 | xchnxbi 332 | 1 ⊢ (¬ 𝜒 ↔ 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ↔ wb 206 | 
| 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 207 | 
| This theorem is referenced by: 3ioran 1106 3ianor 1107 hadnot 1602 cadnot 1615 2exanali 1860 nabbib 3045 nelb 3234 nsspssun 4268 undif3 4300 2nreu 4444 intirr 6138 ordtri3or 6416 nf1const 7324 nf1oconst 7325 frxp 8151 ressuppssdif 8210 suppofssd 8228 naddcllem 8714 domunfican 9361 ssfin4 10350 prinfzo0 13738 swrdnnn0nd 14694 swrdnd0 14695 lcmfunsnlem2lem1 16675 ncoprmlnprm 16765 prm23ge5 16853 smndex2dnrinv 18928 symgfix2 19434 gsumdixp 20316 cnfldfun 21378 cnfldfunOLD 21391 symgmatr01lem 22659 ppttop 23014 zclmncvs 25182 mdegleb 26103 2lgslem3 27448 trlsegvdeg 30246 strlem1 32269 difrab2 32517 isarchi 33189 bnj1189 35023 dfacycgr1 35149 fmlasucdisj 35404 dfon3 35893 wl-3xornot 37482 poimirlem18 37645 poimirlem21 37648 poimirlem30 37657 poimirlem31 37658 ftc1anclem3 37702 hdmaplem4 41776 mapdh9a 41791 onsupmaxb 43251 dflim5 43342 faosnf0.11b 43440 ifpnot23 43491 ifpdfxor 43500 ifpnim1 43510 ifpnim2 43512 dfsucon 43536 ntrneineine1lem 44097 disjrnmpt2 45193 aiotavb 47102 dfatprc 47142 ndmafv2nrn 47234 nfunsnafv2 47237 oddneven 47631 usgrexmpl2trifr 47996 | 
| Copyright terms: Public domain | W3C validator |