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  1085  axpr  5369  relexpindlem  15025  relexpind  15026  axprALT2  35253  unielss  43646  ifpbi2  43894  ifpbi3  43895  3impexpbicom  44907  sbcim2g  44965  3impexpbicomVD  45283  sbcim2gVD  45301  csbeq2gVD  45318  con5VD  45326  hbexgVD  45332  ax6e2ndeqVD  45335  2sb5ndVD  45336  ax6e2ndeqALT  45357  2sb5ndALT  45358