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 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbibiOLD  397  con3ALT  1101  axpr  5396  relexpindlem  15259  relexpind  15260  axprALT2  35857  unielss  44481  ifpbi2  44729  ifpbi3  44730  3impexpbicom  45723  sbcim2g  45781  3impexpbicomVD  46099  sbcim2gVD  46117  csbeq2gVD  46134  con5VD  46142  hbexgVD  46148  ax6e2ndeqVD  46151  2sb5ndVD  46152  ax6e2ndeqALT  46173  2sb5ndALT  46174