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  2876  reu2  2948  reu8  2956  2reuswapdc  2964  2rmorex  2966  dfdif3  3269  ssconb  3292  ssin  3381  reldisj  3498  ssundifim  3530  ralm  3550  unissb  3865  repizf2lem  4190  elirr  4573  en2lp  4586  tfi  4614  ssrel  4747  ssrel2  4749  fncnv  5320  fun11  5321  axcaucvglemres  7959  axpre-suploc  7962  suprzclex  9415  raluz2  9644  supinfneg  9660  infsupneg  9661  infssuzex  12086  bezoutlemmain  12135  isprm2  12255  lmres  14416  ivthdich  14807  limcdifap  14816