Theorem imbi2i 226

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 180	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12i  239  anidmdbi  398  nan  698  sbcof2  1858  sblimv  1943  sbhb  1993  sblim  2010  2sb6  2037  sbcom2v  2038  2sb6rf  2043  eu1  2104  moabs  2129  mo3h  2133  moanim  2154  2moswapdc  2170  r2alf  2549  r19.21t  2607  rspc2gv  2922  reu2  2994  reu8  3002  2reuswapdc  3010  2rmorex  3012  dfdif3  3317  ssconb  3340  ssin  3429  reldisj  3546  ssundifim  3578  ralm  3598  unissb  3923  repizf2lem  4251  elirr  4639  en2lp  4652  tfi  4680  ssrel  4814  ssrel2  4816  fncnv  5396  fun11  5397  axcaucvglemres  8119  axpre-suploc  8122  suprzclex  9578  raluz2  9813  supinfneg  9829  infsupneg  9830  infssuzex  10494  bezoutlemmain  12587  isprm2  12707  lmres  14991  ivthdich  15396  limcdifap  15405