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  5392  relexpindlem  15136  relexpind  15137  axprALT2  35617  unielss  44059  ifpbi2  44307  ifpbi3  44308  3impexpbicom  45303  sbcim2g  45361  3impexpbicomVD  45679  sbcim2gVD  45697  csbeq2gVD  45714  con5VD  45722  hbexgVD  45728  ax6e2ndeqVD  45731  2sb5ndVD  45732  ax6e2ndeqALT  45753  2sb5ndALT  45754