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  807  nan  830  imimorb  953  pm5.6  1004  nannan  1499  alimex  1833  19.36v  1995  2sb6  2092  sbrimvw  2097  sbal  2175  19.36  2238  sbn  2287  sbrim  2311  sblim  2312  cbvsbvf  2367  sbhb  2525  dfmo2  2596  eu1  2610  r2allem  3125  r3al  3175  r19.21t  3231  rspc2gv  3574  reu2  3671  reu8  3679  2reu5lem3  3703  rmoanim  3832  rmoanimALT  3833  dfdif3OLD  4058  ssconb  4082  ssin  4179  difin  4212  reldisj  4393  ssundif  4427  ralidmw  4456  ralidm  4457  reuprg0  4646  raldifsni  4740  pwpw0  4756  unissb  4883  moabexOLD  5411  dffr2  5592  dffr2ALT  5593  dfepfr  5615  ssrel2  5741  dffr3  6064  opreu2reurex  6258  dffr4  6284  fncnv  6571  fun11  6572  dff13  7209  naddssim  8621  marypha2lem3  9350  dfsup2  9357  wemapsolem  9465  inf2  9544  axinf2  9561  aceq1  10039  aceq0  10040  kmlem14  10086  dfackm  10089  zfac  10382  ac6n  10407  zfcndrep  10537  zfcndac  10542  axgroth6  10751  axgroth4  10755  grothprim  10757  prime  12610  raluz2  12847  fsuppmapnn0ub  13957  mptnn0fsuppr  13961  brtrclfv  14964  rpnnen2lem12  16192  isprm2  16651  isprm4  16653  pgpfac1  20057  pgpfac  20061  isirred2  20401  isdomn5  20687  evl1maprhm  22344  pmatcollpw2lem  22742  isclo2  23053  lmres  23265  ist1-2  23312  is1stc2  23407  alexsubALTlem3  24014  itg2cn  25730  ellimc3  25846  plydivex  26263  vieta1  26278  dchrelbas2  27200  conway  27771  nmobndseqi  30850  nmobndseqiALT  30851  cvnbtwn3  32359  elat2  32411  inpr0  32602  ssrelf  32688  isarchi2  33246  archiabl  33259  islinds5  33427  1arithidom  33597  esumcvgre  34235  signstfvneq0  34716  hashreprin  34764  breprexp  34777  bnj1098  34926  bnj1533  34994  bnj121  35012  bnj124  35013  bnj130  35016  bnj153  35022  bnj207  35023  bnj611  35060  bnj864  35064  bnj865  35065  bnj1000  35083  bnj978  35091  bnj1021  35108  bnj1047  35115  bnj1049  35116  bnj1090  35121  bnj1110  35124  bnj1128  35132  bnj1145  35135  bnj1171  35142  bnj1172  35143  bnj1174  35145  bnj1176  35147  bnj1280  35162  axreg  35271  axregscl  35272  axinfprim  35888  dfon2lem9  35971  dffun10  36094  elicc3  36499  filnetlem4  36563  df3nandALT1  36581  df3nandALT2  36582  regsfromregtco  36720  regsfromunir1  36722  mh-infprim2bi  36729  bj-ssbeq  36947  bj-ax12ssb  36952  bj-alnnf  37034  qdiffALT  37642  pibt2  37733  poimirlem30  37971  inxpssidinxp  38643  cnvref5  38672  lcvnbtwn3  39474  isat3  39753  cdleme25cv  40804  cdlemefrs29bpre0  40842  cdlemk35  41358  dvrelogpow2b  42507  aks4d1p1p4  42510  aks6d1c2p2  42558  aks5lem3a  42628  aks5lem6  42631  unitscyglem2  42635  unitscyglem3  42636  sn-axrep5v  42658  supinf  42681  dford4  43457  ifpidg  43918  ifpid1g  43921  ifpim23g  43922  ifpororb  43932  ifpbibib  43937  elinintrab  44004  undmrnresiss  44031  cotrintab  44041  elintima  44080  frege60b  44332  frege91  44381  frege97  44387  frege98  44388  dffrege99  44389  frege109  44399  frege110  44400  frege131  44421  frege133  44423  ntrneiiso  44518  int-sqdefd  44608  int-sqgeq0d  44613  ismnuprim  44721  pm10.541  44794  pm13.196a  44841  2sbc6g  44842  expcomdg  44927  impexpd  44940  supxrleubrnmptf  45879  fsummulc1f  46001  fsumiunss  46005  fnlimfvre2  46105  limsupreuz  46165  lmbr3v  46173  dvmptmulf  46365  dvmptfprodlem  46372  sge0ltfirpmpt2  46854  hoidmv1le  47022  hoidmvle  47028  vonioolem2  47109  smflimlem3  47201  ldepslinc  48985  map0cor  49330  setrec1lem2  50163  setrec2  50170  sbidd-misc  50194