![]() |
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 eqabw 2814 eqabOLD 2879 eqabf 2941 pm13.183 3619 dfss2 3931 eq0 4304 eq0rdv 4365 disj 4408 disj3 4414 rzal 4467 axrep5 5249 axrep6 5250 axsepgfromrep 5255 ax6vsep 5261 inex1 5275 axprALT 5378 zfpair2 5386 sucel 6392 suppvalbr 8097 bnj89 33336 fineqvrep 33699 axrepprim 34276 brtxpsd3 34484 bisym1 34894 bj-bixor 35059 eliminable-veqab 35335 bj-snsetex 35437 bj-reabeq 35501 bj-clex 35505 wl-3xorbi 35947 sn-axrep5v 40641 ifpidg 41770 nanorxor 42592 mo0sn 46907 |
Copyright terms: Public domain | W3C validator |