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 | ||
|---|---|---|---|
| Hypothesis | bibi2i.1 | |- ( ph <-> ps ) |
|
| Assertion | bibi2i | |- ( ( ch <-> ph ) <-> ( ch <-> ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bibi2i.1 | |- ( ph <-> ps ) |
|
| 2 | id | |- ( ( ch <-> ph ) -> ( ch <-> ph ) ) |
|
| 3 | 2 1 | bitrdi | |- ( ( ch <-> ph ) -> ( ch <-> ps ) ) |
| 4 | id | |- ( ( ch <-> ps ) -> ( ch <-> ps ) ) |
|
| 5 | 4 1 | bitr4di | |- ( ( ch <-> ps ) -> ( ch <-> ph ) ) |
| 6 | 3 5 | impbii | |- ( ( ch <-> ph ) <-> ( ch <-> ps ) ) |