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: con3ALT 1084 relexpindlem 14774 relexpind 14775 ifpbi2 41074 ifpbi3 41075 3impexpbicom 42099 sbcim2g 42158 3impexpbicomVD 42477 sbcim2gVD 42495 csbeq2gVD 42512 con5VD 42520 hbexgVD 42526 ax6e2ndeqVD 42529 2sb5ndVD 42530 ax6e2ndeqALT 42551 2sb5ndALT 42552 |
Copyright terms: Public domain | W3C validator |