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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imbi12i  239  anidmdbi  402  nan  703  sbcof2  1863  sblimv  1950  sbhb  2000  sblim  2017  2sb6  2044  sbcom2v  2045  2sb6rf  2050  eu1  2111  moabs  2136  mo3h  2140  moanim  2161  2moswapdc  2177  r2alf  2567  r19.21t  2625  rspc2gv  2942  reu2  3014  reu8  3022  2reuswapdc  3030  2rmorex  3032  dfdif3  3339  ssconb  3362  ssin  3453  reldisj  3576  ssundifim  3611  ralm  3631  unissb  3965  repizf2lem  4298  elirr  4688  en2lp  4701  tfi  4729  ssrel  4863  ssrel2  4865  fncnv  5447  fun11  5448  axcaucvglemres  8267  axpre-suploc  8270  suprzclex  9749  raluz2  9989  supinfneg  10005  infsupneg  10006  infssuzex  10677  bezoutlemmain  12794  isprm2  12914  lmres  15440  ivthdich  15845  limcdifap  15854