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  5389  relexpindlem  15225  relexpind  15226  axprALT2  35790  unielss  44329  ifpbi2  44577  ifpbi3  44578  3impexpbicom  45571  sbcim2g  45629  3impexpbicomVD  45947  sbcim2gVD  45965  csbeq2gVD  45982  con5VD  45990  hbexgVD  45996  ax6e2ndeqVD  45999  2sb5ndVD  46000  ax6e2ndeqALT  46021  2sb5ndALT  46022