![]() |
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 208 | 1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ 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: bibi1i 339 bibi12i 340 bibi2d 343 con2bi 354 pm4.71r 560 xorass 1515 sblbis 2306 sbrbif 2308 eqabbw 2810 eqabbOLD 2875 eqabf 2936 pm13.183 3657 dfss2 3969 eq0 4344 eq0rdv 4405 disj 4448 disj3 4454 rzal 4509 axrep5 5292 axrep6 5293 axsepgfromrep 5298 ax6vsep 5304 inex1 5318 axprALT 5421 zfpair2 5429 sucel 6439 suppvalbr 8150 bnj89 33732 fineqvrep 34095 axrepprim 34671 brtxpsd3 34868 bisym1 35304 bj-bixor 35469 eliminable-veqab 35745 bj-snsetex 35844 bj-reabeq 35908 bj-clex 35912 wl-3xorbi 36354 sn-axrep5v 41033 ifpidg 42242 nanorxor 43064 mo0sn 47500 |
Copyright terms: Public domain | W3C validator |