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  5400  relexpindlem  15124  relexpind  15125  axprALT2  35561  unielss  44003  ifpbi2  44251  ifpbi3  44252  3impexpbicom  45247  sbcim2g  45305  3impexpbicomVD  45623  sbcim2gVD  45641  csbeq2gVD  45658  con5VD  45666  hbexgVD  45672  ax6e2ndeqVD  45675  2sb5ndVD  45676  ax6e2ndeqALT  45697  2sb5ndALT  45698