Theorem imbi2i 215

Description: Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)

Hypothesis

Ref	Expression
bi.a	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
imbi2i	⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		bi.a	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 169	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  imbi12i  228  anidmdbi  378  nan  626  sbcof2  1691  sblimv  1774  sbhb  1816  sblim  1831  2sb6  1860  sbcom2v  1861  2sb6rf  1866  eu1  1925  moabs  1949  mo3h  1953  moanim  1974  2moswapdc  1990  r2alf  2341  r19.21t  2394  reu2  2729  reu8  2737  2reuswapdc  2743  2rmorex  2745  ssconb  3076  ssin  3159  reldisj  3271  ssundifim  3306  ralm  3325  unissb  3610  repizf2lem  3914  elirr  4266  en2lp  4278  tfi  4305  ssrel  4428  ssrel2  4430  fncnv  4965  fun11  4966  axcaucvglemres  6973  raluz2  8522