Theorem imbi2 351

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 23	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 ↔ 𝜓))
2	1	imbi2d 343	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imbibiOLD  396  con3ALT  1101  axpr  5398  relexpindlem  15096  relexpind  15097  axprALT2  35503  unielss  43945  ifpbi2  44193  ifpbi3  44194  3impexpbicom  45189  sbcim2g  45247  3impexpbicomVD  45565  sbcim2gVD  45583  csbeq2gVD  45600  con5VD  45608  hbexgVD  45614  ax6e2ndeqVD  45617  2sb5ndVD  45618  ax6e2ndeqALT  45639  2sb5ndALT  45640