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  693  sbcof2  1821  sblimv  1906  sbhb  1956  sblim  1973  2sb6  2000  sbcom2v  2001  2sb6rf  2006  eu1  2067  moabs  2091  mo3h  2095  moanim  2116  2moswapdc  2132  r2alf  2511  r19.21t  2569  rspc2gv  2877  reu2  2949  reu8  2957  2reuswapdc  2965  2rmorex  2967  dfdif3  3270  ssconb  3293  ssin  3382  reldisj  3499  ssundifim  3531  ralm  3551  unissb  3866  repizf2lem  4191  elirr  4574  en2lp  4587  tfi  4615  ssrel  4748  ssrel2  4750  fncnv  5321  fun11  5322  axcaucvglemres  7961  axpre-suploc  7964  suprzclex  9418  raluz2  9647  supinfneg  9663  infsupneg  9664  infssuzex  12089  bezoutlemmain  12138  isprm2  12258  lmres  14427  ivthdich  14832  limcdifap  14841