![]() |
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 1084 axpr 5433 relexpindlem 15099 relexpind 15100 unielss 43207 ifpbi2 43457 ifpbi3 43458 3impexpbicom 44477 sbcim2g 44536 3impexpbicomVD 44855 sbcim2gVD 44873 csbeq2gVD 44890 con5VD 44898 hbexgVD 44904 ax6e2ndeqVD 44907 2sb5ndVD 44908 ax6e2ndeqALT 44929 2sb5ndALT 44930 |
Copyright terms: Public domain | W3C validator |