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 342 | 1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: con3ALT 1076 relexpindlem 14410 relexpind 14411 ifpbi2 39710 ifpbi3 39711 3impexpbicom 40690 sbcim2g 40749 3impexpbicomVD 41068 sbcim2gVD 41086 csbeq2gVD 41103 con5VD 41111 hbexgVD 41117 ax6e2ndeqVD 41120 2sb5ndVD 41121 ax6e2ndeqALT 41142 2sb5ndALT 41143 |
Copyright terms: Public domain | W3C validator |