| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > imbi2 | Structured version Visualization version GIF version | ||
| Description: Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
| Ref | Expression |
|---|---|
| imbi2 | ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 ↔ 𝜓)) | |
| 2 | 1 | imbi2d 340 | 1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ 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: imbibi 391 con3ALT 1085 axpr 5427 relexpindlem 15102 relexpind 15103 unielss 43230 ifpbi2 43480 ifpbi3 43481 3impexpbicom 44500 sbcim2g 44558 3impexpbicomVD 44877 sbcim2gVD 44895 csbeq2gVD 44912 con5VD 44920 hbexgVD 44926 ax6e2ndeqVD 44929 2sb5ndVD 44930 ax6e2ndeqALT 44951 2sb5ndALT 44952 |
| Copyright terms: Public domain | W3C validator |