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  15209  relexpind  15210  axprALT2  35723  unielss  44204  ifpbi2  44452  ifpbi3  44453  3impexpbicom  45448  sbcim2g  45506  3impexpbicomVD  45824  sbcim2gVD  45842  csbeq2gVD  45859  con5VD  45867  hbexgVD  45873  ax6e2ndeqVD  45876  2sb5ndVD  45877  ax6e2ndeqALT  45898  2sb5ndALT  45899