Theorem imbi2 348

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 340	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))

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  5397  relexpindlem  15082  relexpind  15083  unielss  43242  ifpbi2  43491  ifpbi3  43492  3impexpbicom  44505  sbcim2g  44563  3impexpbicomVD  44881  sbcim2gVD  44899  csbeq2gVD  44916  con5VD  44924  hbexgVD  44930  ax6e2ndeqVD  44933  2sb5ndVD  44934  ax6e2ndeqALT  44955  2sb5ndALT  44956