![]() |
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 341 | 1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ 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: imbibi 393 con3ALT 1086 relexpindlem 15007 relexpind 15008 unielss 41953 ifpbi2 42204 ifpbi3 42205 3impexpbicom 43226 sbcim2g 43285 3impexpbicomVD 43604 sbcim2gVD 43622 csbeq2gVD 43639 con5VD 43647 hbexgVD 43653 ax6e2ndeqVD 43656 2sb5ndVD 43657 ax6e2ndeqALT 43678 2sb5ndALT 43679 |
Copyright terms: Public domain | W3C validator |