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  2362  sbhb  2520  dfmo  2590  eu1  2604  r2allem  3122  r19.21vOLD  3160  r3al  3176  r19.21t  3232  rspc2gv  3601  reu2  3698  reu8  3706  2reu5lem3  3730  rmoanim  3859  rmoanimALT  3860  dfdif3OLD  4083  ssconb  4107  ssin  4204  difin  4237  reldisj  4418  ssundif  4453  ralidmw  4473  ralidm  4477  reuprg0  4668  raldifsni  4761  pwpw0  4779  unissb  4905  unissbOLD  4906  moabex  5421  dffr2  5601  dffr2ALT  5602  dfepfr  5624  ssrel2  5750  dffr3  6072  opreu2reurex  6269  dffr4  6295  fncnv  6591  fun11  6592  dff13  7231  naddssim  8651  marypha2lem3  9394  dfsup2  9401  wemapsolem  9509  inf2  9582  axinf2  9599  aceq1  10076  aceq0  10077  kmlem14  10123  dfackm  10126  zfac  10419  ac6n  10444  zfcndrep  10573  zfcndac  10578  axgroth6  10787  axgroth4  10791  grothprim  10793  prime  12621  raluz2  12862  fsuppmapnn0ub  13966  mptnn0fsuppr  13970  brtrclfv  14974  rpnnen2lem12  16199  isprm2  16658  isprm4  16660  pgpfac1  20018  pgpfac  20022  isirred2  20336  isdomn5  20625  evl1maprhm  22272  pmatcollpw2lem  22670  isclo2  22981  lmres  23193  ist1-2  23240  is1stc2  23335  alexsubALTlem3  23942  itg2cn  25670  ellimc3  25786  plydivex  26211  vieta1  26226  dchrelbas2  27154  conway  27717  nmobndseqi  30714  nmobndseqiALT  30715  cvnbtwn3  32223  elat2  32275  inpr0  32467  ssrelf  32549  isarchi2  33145  archiabl  33158  islinds5  33344  1arithidom  33514  esumcvgre  34087  signstfvneq0  34569  hashreprin  34617  breprexp  34630  bnj1098  34779  bnj1533  34848  bnj121  34866  bnj124  34867  bnj130  34870  bnj153  34876  bnj207  34877  bnj611  34914  bnj864  34918  bnj865  34919  bnj1000  34937  bnj978  34945  bnj1021  34962  bnj1047  34969  bnj1049  34970  bnj1090  34975  bnj1110  34978  bnj1128  34986  bnj1145  34989  bnj1171  34996  bnj1172  34997  bnj1174  34999  bnj1176  35001  bnj1280  35016  axinfprim  35688  dfon2lem9  35774  dffun10  35897  elicc3  36300  filnetlem4  36364  df3nandALT1  36382  df3nandALT2  36383  bj-ssbeq  36636  bj-ax12ssb  36641  pibt2  37400  poimirlem30  37639  inxpssidinxp  38299  cnvref5  38328  lcvnbtwn3  39016  isat3  39295  cdleme25cv  40347  cdlemefrs29bpre0  40385  cdlemk35  40901  dvrelogpow2b  42051  aks4d1p1p4  42054  aks6d1c2p2  42102  aks5lem3a  42172  aks5lem6  42175  unitscyglem2  42179  unitscyglem3  42180  sn-axrep5v  42199  supinf  42225  dford4  43011  ifpidg  43473  ifpid1g  43476  ifpim23g  43477  ifpororb  43487  ifpbibib  43492  elinintrab  43559  undmrnresiss  43586  cotrintab  43596  elintima  43635  frege60b  43887  frege91  43936  frege97  43942  frege98  43943  dffrege99  43944  frege109  43954  frege110  43955  frege131  43976  frege133  43978  ntrneiiso  44073  int-sqdefd  44163  int-sqgeq0d  44168  ismnuprim  44276  pm10.541  44349  pm13.196a  44396  2sbc6g  44397  expcomdg  44483  impexpd  44496  supxrleubrnmptf  45440  fsummulc1f  45562  fsumiunss  45566  fnlimfvre2  45668  limsupreuz  45728  lmbr3v  45736  dvmptmulf  45928  dvmptfprodlem  45935  sge0ltfirpmpt2  46417  hoidmv1le  46585  hoidmvle  46591  vonioolem2  46672  smflimlem3  46764  ldepslinc  48488  map0cor  48833  setrec1lem2  49667  setrec2  49674  sbidd-misc  49698