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  5364  relexpindlem  15016  relexpind  15017  axprALT2  35269  unielss  43664  ifpbi2  43912  ifpbi3  43913  3impexpbicom  44925  sbcim2g  44983  3impexpbicomVD  45301  sbcim2gVD  45319  csbeq2gVD  45336  con5VD  45344  hbexgVD  45350  ax6e2ndeqVD  45353  2sb5ndVD  45354  ax6e2ndeqALT  45375  2sb5ndALT  45376