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  5427  relexpindlem  15102  relexpind  15103  unielss  43230  ifpbi2  43480  ifpbi3  43481  3impexpbicom  44500  sbcim2g  44558  3impexpbicomVD  44877  sbcim2gVD  44895  csbeq2gVD  44912  con5VD  44920  hbexgVD  44926  ax6e2ndeqVD  44929  2sb5ndVD  44930  ax6e2ndeqALT  44951  2sb5ndALT  44952