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  5388  relexpindlem  15216  relexpind  15217  axprALT2  35776  unielss  44262  ifpbi2  44510  ifpbi3  44511  3impexpbicom  45505  sbcim2g  45563  3impexpbicomVD  45881  sbcim2gVD  45899  csbeq2gVD  45916  con5VD  45924  hbexgVD  45930  ax6e2ndeqVD  45933  2sb5ndVD  45934  ax6e2ndeqALT  45955  2sb5ndALT  45956