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  15014  relexpind  15015  unielss  42269  ifpbi2  42520  ifpbi3  42521  3impexpbicom  43542  sbcim2g  43601  3impexpbicomVD  43920  sbcim2gVD  43938  csbeq2gVD  43955  con5VD  43963  hbexgVD  43969  ax6e2ndeqVD  43972  2sb5ndVD  43973  ax6e2ndeqALT  43994  2sb5ndALT  43995