Theorem imbi2 352

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 344	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:  con3ALT  1086  relexpindlem  14524  relexpind  14525  ifpbi2  40668  ifpbi3  40669  3impexpbicom  41677  sbcim2g  41736  3impexpbicomVD  42055  sbcim2gVD  42073  csbeq2gVD  42090  con5VD  42098  hbexgVD  42104  ax6e2ndeqVD  42107  2sb5ndVD  42108  ax6e2ndeqALT  42129  2sb5ndALT  42130