Theorem imbi2 349

Description: Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Assertion

Ref	Expression
imbi2	⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))

Proof of Theorem imbi2

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 ↔ 𝜓))
2	1	imbi2d 341	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))

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