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 344 | 1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 |
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 210 |
This theorem is referenced by: con3ALT 1086 relexpindlem 14524 relexpind 14525 ifpbi2 40668 ifpbi3 40669 3impexpbicom 41677 sbcim2g 41736 3impexpbicomVD 42055 sbcim2gVD 42073 csbeq2gVD 42090 con5VD 42098 hbexgVD 42104 ax6e2ndeqVD 42107 2sb5ndVD 42108 ax6e2ndeqALT 42129 2sb5ndALT 42130 |
Copyright terms: Public domain | W3C validator |