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  5385  relexpindlem  15036  relexpind  15037  unielss  43214  ifpbi2  43463  ifpbi3  43464  3impexpbicom  44477  sbcim2g  44535  3impexpbicomVD  44853  sbcim2gVD  44871  csbeq2gVD  44888  con5VD  44896  hbexgVD  44902  ax6e2ndeqVD  44905  2sb5ndVD  44906  ax6e2ndeqALT  44927  2sb5ndALT  44928