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  5372  relexpindlem  14986  relexpind  14987  unielss  43460  ifpbi2  43708  ifpbi3  43709  3impexpbicom  44721  sbcim2g  44779  3impexpbicomVD  45097  sbcim2gVD  45115  csbeq2gVD  45132  con5VD  45140  hbexgVD  45146  ax6e2ndeqVD  45149  2sb5ndVD  45150  ax6e2ndeqALT  45171  2sb5ndALT  45172