Theorem imbi2 349

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 341	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  imbibi  392  con3ALT  1090  axpr  5356  relexpindlem  15016  relexpind  15017  axprALT2  35290  unielss  43663  ifpbi2  43911  ifpbi3  43912  3impexpbicom  44924  sbcim2g  44982  3impexpbicomVD  45300  sbcim2gVD  45318  csbeq2gVD  45335  con5VD  45343  hbexgVD  45349  ax6e2ndeqVD  45352  2sb5ndVD  45353  ax6e2ndeqALT  45374  2sb5ndALT  45375