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  r19.21vOLD  3159  r3al  3175  r19.21t  3231  rspc2gv  3598  reu2  3696  reu8  3704  2reu5lem3  3728  rmoanim  3857  rmoanimALT  3858  dfdif3OLD  4081  ssconb  4105  ssin  4202  difin  4235  reldisj  4416  ssundif  4451  ralidmw  4471  ralidm  4475  reuprg0  4666  raldifsni  4759  pwpw0  4777  unissb  4903  unissbOLD  4904  moabex  5419  dffr2  5599  dffr2ALT  5600  dfepfr  5622  ssrel2  5748  dffr3  6070  opreu2reurex  6267  dffr4  6293  fncnv  6589  fun11  6590  dff13  7229  naddssim  8649  marypha2lem3  9388  dfsup2  9395  wemapsolem  9503  inf2  9576  axinf2  9593  aceq1  10070  aceq0  10071  kmlem14  10117  dfackm  10120  zfac  10413  ac6n  10438  zfcndrep  10567  zfcndac  10572  axgroth6  10781  axgroth4  10785  grothprim  10787  prime  12615  raluz2  12856  fsuppmapnn0ub  13960  mptnn0fsuppr  13964  brtrclfv  14968  rpnnen2lem12  16193  isprm2  16652  isprm4  16654  pgpfac1  20012  pgpfac  20016  isirred2  20330  isdomn5  20619  evl1maprhm  22266  pmatcollpw2lem  22664  isclo2  22975  lmres  23187  ist1-2  23234  is1stc2  23329  alexsubALTlem3  23936  itg2cn  25664  ellimc3  25780  plydivex  26205  vieta1  26220  dchrelbas2  27148  conway  27711  nmobndseqi  30708  nmobndseqiALT  30709  cvnbtwn3  32217  elat2  32269  inpr0  32461  ssrelf  32543  isarchi2  33139  archiabl  33152  islinds5  33338  1arithidom  33508  esumcvgre  34081  signstfvneq0  34563  hashreprin  34611  breprexp  34624  bnj1098  34773  bnj1533  34842  bnj121  34860  bnj124  34861  bnj130  34864  bnj153  34870  bnj207  34871  bnj611  34908  bnj864  34912  bnj865  34913  bnj1000  34931  bnj978  34939  bnj1021  34956  bnj1047  34963  bnj1049  34964  bnj1090  34969  bnj1110  34972  bnj1128  34980  bnj1145  34983  bnj1171  34990  bnj1172  34991  bnj1174  34993  bnj1176  34995  bnj1280  35010  axinfprim  35693  dfon2lem9  35779  dffun10  35902  elicc3  36305  filnetlem4  36369  df3nandALT1  36387  df3nandALT2  36388  bj-ssbeq  36641  bj-ax12ssb  36646  pibt2  37405  poimirlem30  37644  inxpssidinxp  38304  cnvref5  38333  lcvnbtwn3  39021  isat3  39300  cdleme25cv  40352  cdlemefrs29bpre0  40390  cdlemk35  40906  dvrelogpow2b  42056  aks4d1p1p4  42059  aks6d1c2p2  42107  aks5lem3a  42177  aks5lem6  42180  unitscyglem2  42184  unitscyglem3  42185  sn-axrep5v  42204  supinf  42230  dford4  43018  ifpidg  43480  ifpid1g  43483  ifpim23g  43484  ifpororb  43494  ifpbibib  43499  elinintrab  43566  undmrnresiss  43593  cotrintab  43603  elintima  43642  frege60b  43894  frege91  43943  frege97  43949  frege98  43950  dffrege99  43951  frege109  43961  frege110  43962  frege131  43983  frege133  43985  ntrneiiso  44080  int-sqdefd  44170  int-sqgeq0d  44175  ismnuprim  44283  pm10.541  44356  pm13.196a  44403  2sbc6g  44404  expcomdg  44490  impexpd  44503  supxrleubrnmptf  45447  fsummulc1f  45569  fsumiunss  45573  fnlimfvre2  45675  limsupreuz  45735  lmbr3v  45743  dvmptmulf  45935  dvmptfprodlem  45942  sge0ltfirpmpt2  46424  hoidmv1le  46592  hoidmvle  46598  vonioolem2  46679  smflimlem3  46771  ldepslinc  48498  map0cor  48843  setrec1lem2  49677  setrec2  49684  sbidd-misc  49708