Theorem imbi2i 336

Description: Introduce an antecedent to both sides of a logical equivalence. This and the next three rules are useful for building up wff's around a definition, in order to make use of the definition. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)

Hypothesis

Ref	Expression
imbi2i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

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

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		imbi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 271	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  iman  401  anidmdbi  565  pm5.32  573  pm4.14  806  nan  829  imimorb  952  pm5.6  1003  nannan  1497  alimex  1831  19.36v  1993  2sb6  2087  sbrimvw  2092  sbal  2170  19.36  2231  sbn  2280  sbrim  2304  sblim  2305  sbnfOLD  2312  cbvsbvf  2361  sbhb  2519  dfmo  2589  eu1  2603  r2allem  3121  r3al  3173  r19.21t  3229  rspc2gv  3595  reu2  3693  reu8  3701  2reu5lem3  3725  rmoanim  3854  rmoanimALT  3855  dfdif3OLD  4077  ssconb  4101  ssin  4198  difin  4231  reldisj  4412  ssundif  4447  ralidmw  4467  ralidm  4471  reuprg0  4662  raldifsni  4755  pwpw0  4773  unissb  4899  unissbOLD  4900  moabex  5414  dffr2  5592  dffr2ALT  5593  dfepfr  5615  ssrel2  5739  dffr3  6059  opreu2reurex  6255  dffr4  6281  fncnv  6573  fun11  6574  dff13  7211  naddssim  8626  marypha2lem3  9364  dfsup2  9371  wemapsolem  9479  inf2  9552  axinf2  9569  aceq1  10046  aceq0  10047  kmlem14  10093  dfackm  10096  zfac  10389  ac6n  10414  zfcndrep  10543  zfcndac  10548  axgroth6  10757  axgroth4  10761  grothprim  10763  prime  12591  raluz2  12832  fsuppmapnn0ub  13936  mptnn0fsuppr  13940  brtrclfv  14944  rpnnen2lem12  16169  isprm2  16628  isprm4  16630  pgpfac1  19988  pgpfac  19992  isirred2  20306  isdomn5  20595  evl1maprhm  22242  pmatcollpw2lem  22640  isclo2  22951  lmres  23163  ist1-2  23210  is1stc2  23305  alexsubALTlem3  23912  itg2cn  25640  ellimc3  25756  plydivex  26181  vieta1  26196  dchrelbas2  27124  conway  27687  nmobndseqi  30681  nmobndseqiALT  30682  cvnbtwn3  32190  elat2  32242  inpr0  32434  ssrelf  32516  isarchi2  33112  archiabl  33125  islinds5  33311  1arithidom  33481  esumcvgre  34054  signstfvneq0  34536  hashreprin  34584  breprexp  34597  bnj1098  34746  bnj1533  34815  bnj121  34833  bnj124  34834  bnj130  34837  bnj153  34843  bnj207  34844  bnj611  34881  bnj864  34885  bnj865  34886  bnj1000  34904  bnj978  34912  bnj1021  34929  bnj1047  34936  bnj1049  34937  bnj1090  34942  bnj1110  34945  bnj1128  34953  bnj1145  34956  bnj1171  34963  bnj1172  34964  bnj1174  34966  bnj1176  34968  bnj1280  34983  axinfprim  35666  dfon2lem9  35752  dffun10  35875  elicc3  36278  filnetlem4  36342  df3nandALT1  36360  df3nandALT2  36361  bj-ssbeq  36614  bj-ax12ssb  36619  pibt2  37378  poimirlem30  37617  inxpssidinxp  38277  cnvref5  38306  lcvnbtwn3  38994  isat3  39273  cdleme25cv  40325  cdlemefrs29bpre0  40363  cdlemk35  40879  dvrelogpow2b  42029  aks4d1p1p4  42032  aks6d1c2p2  42080  aks5lem3a  42150  aks5lem6  42153  unitscyglem2  42157  unitscyglem3  42158  sn-axrep5v  42177  supinf  42203  dford4  42991  ifpidg  43453  ifpid1g  43456  ifpim23g  43457  ifpororb  43467  ifpbibib  43472  elinintrab  43539  undmrnresiss  43566  cotrintab  43576  elintima  43615  frege60b  43867  frege91  43916  frege97  43922  frege98  43923  dffrege99  43924  frege109  43934  frege110  43935  frege131  43956  frege133  43958  ntrneiiso  44053  int-sqdefd  44143  int-sqgeq0d  44148  ismnuprim  44256  pm10.541  44329  pm13.196a  44376  2sbc6g  44377  expcomdg  44463  impexpd  44476  supxrleubrnmptf  45420  fsummulc1f  45542  fsumiunss  45546  fnlimfvre2  45648  limsupreuz  45708  lmbr3v  45716  dvmptmulf  45908  dvmptfprodlem  45915  sge0ltfirpmpt2  46397  hoidmv1le  46565  hoidmvle  46571  vonioolem2  46652  smflimlem3  46744  ldepslinc  48471  map0cor  48816  setrec1lem2  49650  setrec2  49657  sbidd-misc  49681