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 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:  con3ALT  1083  relexpindlem  14702  relexpind  14703  ifpbi2  40972  ifpbi3  40973  3impexpbicom  41988  sbcim2g  42047  3impexpbicomVD  42366  sbcim2gVD  42384  csbeq2gVD  42401  con5VD  42409  hbexgVD  42415  ax6e2ndeqVD  42418  2sb5ndVD  42419  ax6e2ndeqALT  42440  2sb5ndALT  42441