Theorem imbi2 350

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  imbibiOLD  395  con3ALT  1096  axpr  5384  relexpindlem  15076  relexpind  15077  axprALT2  35402  unielss  43792  ifpbi2  44040  ifpbi3  44041  3impexpbicom  45053  sbcim2g  45111  3impexpbicomVD  45429  sbcim2gVD  45447  csbeq2gVD  45464  con5VD  45472  hbexgVD  45478  ax6e2ndeqVD  45481  2sb5ndVD  45482  ax6e2ndeqALT  45503  2sb5ndALT  45504