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 205

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 206

This theorem is referenced by:  imbibi  392  con3ALT  1085  relexpindlem  14960  relexpind  14961  unielss  41610  ifpbi2  41861  ifpbi3  41862  3impexpbicom  42883  sbcim2g  42942  3impexpbicomVD  43261  sbcim2gVD  43279  csbeq2gVD  43296  con5VD  43304  hbexgVD  43310  ax6e2ndeqVD  43313  2sb5ndVD  43314  ax6e2ndeqALT  43335  2sb5ndALT  43336