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 22	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 ↔ 𝜓))
2	1	imbi2d 343	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  con3ALT  1080  relexpindlem  14424  relexpind  14425  ifpbi2  39839  ifpbi3  39840  3impexpbicom  40820  sbcim2g  40879  3impexpbicomVD  41198  sbcim2gVD  41216  csbeq2gVD  41233  con5VD  41241  hbexgVD  41247  ax6e2ndeqVD  41250  2sb5ndVD  41251  ax6e2ndeqALT  41272  2sb5ndALT  41273