Theorem imbi2 351

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 23	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 ↔ 𝜓))
2	1	imbi2d 343	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:  imbibiOLD  396  con3ALT  1099  axpr  5399  relexpindlem  15099  relexpind  15100  axprALT2  35444  unielss  43836  ifpbi2  44084  ifpbi3  44085  3impexpbicom  45080  sbcim2g  45138  3impexpbicomVD  45456  sbcim2gVD  45474  csbeq2gVD  45491  con5VD  45499  hbexgVD  45505  ax6e2ndeqVD  45508  2sb5ndVD  45509  ax6e2ndeqALT  45530  2sb5ndALT  45531