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  5374  relexpindlem  14998  relexpind  14999  axprALT2  35287  unielss  43575  ifpbi2  43823  ifpbi3  43824  3impexpbicom  44836  sbcim2g  44894  3impexpbicomVD  45212  sbcim2gVD  45230  csbeq2gVD  45247  con5VD  45255  hbexgVD  45261  ax6e2ndeqVD  45264  2sb5ndVD  45265  ax6e2ndeqALT  45286  2sb5ndALT  45287