| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > bibi2i | Structured version Visualization version GIF version | ||
| Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.) |
| Ref | Expression |
|---|---|
| bibi2i.1 | ⊢ (𝜑 ↔ 𝜓) |
| Ref | Expression |
|---|---|
| bibi2i | ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . . 3 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜑)) | |
| 2 | bibi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
| 3 | 1, 2 | bitrdi 287 | . 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓)) |
| 4 | id 22 | . . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓)) | |
| 5 | 4, 2 | bitr4di 289 | . 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑)) |
| 6 | 3, 5 | impbii 209 | 1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ 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: bibi1i 338 bibi12i 339 bibi2d 342 con2bi 353 pm4.71r 558 xorass 1515 sblbis 2309 sbrbif 2311 eqabbw 2815 eqabbOLD 2882 eqabf 2935 eq0 4350 eq0rdv 4407 disj 4450 disj3 4454 rzal 4509 axrep4v 5284 axrep4 5285 axrep5 5287 axrep6 5288 axrep6OLD 5289 axsepgfromrep 5294 ax6vsep 5303 inex1 5317 axprALT 5422 zfpair2 5433 sucel 6458 suppvalbr 8189 bnj89 34735 fineqvrep 35109 axrepprim 35702 brtxpsd3 35897 bisym1 36420 bj-bixor 36592 eliminable-veqab 36867 bj-snsetex 36964 bj-reabeq 37028 bj-clex 37032 wl-3xorbi 37474 sn-axrep5v 42255 ifpidg 43504 nanorxor 44324 mo0sn 48735 |
| Copyright terms: Public domain | W3C validator |