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 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  393  con3ALT  1086  relexpindlem  15007  relexpind  15008  unielss  41953  ifpbi2  42204  ifpbi3  42205  3impexpbicom  43226  sbcim2g  43285  3impexpbicomVD  43604  sbcim2gVD  43622  csbeq2gVD  43639  con5VD  43647  hbexgVD  43653  ax6e2ndeqVD  43656  2sb5ndVD  43657  ax6e2ndeqALT  43678  2sb5ndALT  43679