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  5366  relexpindlem  14970  relexpind  14971  unielss  43191  ifpbi2  43440  ifpbi3  43441  3impexpbicom  44454  sbcim2g  44512  3impexpbicomVD  44830  sbcim2gVD  44848  csbeq2gVD  44865  con5VD  44873  hbexgVD  44879  ax6e2ndeqVD  44882  2sb5ndVD  44883  ax6e2ndeqALT  44904  2sb5ndALT  44905