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  1084  axpr  5370  relexpindlem  14984  relexpind  14985  unielss  43402  ifpbi2  43650  ifpbi3  43651  3impexpbicom  44663  sbcim2g  44721  3impexpbicomVD  45039  sbcim2gVD  45057  csbeq2gVD  45074  con5VD  45082  hbexgVD  45088  ax6e2ndeqVD  45091  2sb5ndVD  45092  ax6e2ndeqALT  45113  2sb5ndALT  45114