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  1497  alimex  1831  19.36v  1987  2sb6  2086  sbrimvw  2091  sbal  2169  19.36  2230  sbn  2280  sbrim  2304  sblim  2306  sbnfOLD  2313  cbvsbvf  2366  sbhb  2526  dfmo  2596  eu1  2610  r2allem  3142  r19.21vOLD  3181  r3al  3197  r19.21t  3253  nfra2wOLD  3300  rspc2gv  3632  reu2  3731  reu8  3739  2reu5lem3  3763  rmoanim  3894  rmoanimALT  3895  dfdif3OLD  4118  ssconb  4142  ssin  4239  difin  4272  reldisj  4453  ssundif  4488  ralidmw  4508  ralidm  4512  reuprg0  4702  raldifsni  4795  pwpw0  4813  unissb  4939  unissbOLD  4940  moabex  5464  dffr2  5646  dffr2ALT  5647  dfepfr  5669  ssrel2  5795  dffr3  6117  opreu2reurex  6314  dffr4  6341  fncnv  6639  fun11  6640  dff13  7275  naddssim  8723  marypha2lem3  9477  dfsup2  9484  wemapsolem  9590  inf2  9663  axinf2  9680  aceq1  10157  aceq0  10158  kmlem14  10204  dfackm  10207  zfac  10500  ac6n  10525  zfcndrep  10654  zfcndac  10659  axgroth6  10868  axgroth4  10872  grothprim  10874  prime  12699  raluz2  12939  fsuppmapnn0ub  14036  mptnn0fsuppr  14040  brtrclfv  15041  rpnnen2lem12  16261  isprm2  16719  isprm4  16721  pgpfac1  20100  pgpfac  20104  isirred2  20421  isdomn5  20710  evl1maprhm  22383  pmatcollpw2lem  22783  isclo2  23096  lmres  23308  ist1-2  23355  is1stc2  23450  alexsubALTlem3  24057  itg2cn  25798  ellimc3  25914  plydivex  26339  vieta1  26354  dchrelbas2  27281  conway  27844  nmobndseqi  30798  nmobndseqiALT  30799  cvnbtwn3  32307  elat2  32359  inpr0  32550  ssrelf  32627  isarchi2  33192  archiabl  33205  islinds5  33395  1arithidom  33565  esumcvgre  34092  signstfvneq0  34587  hashreprin  34635  breprexp  34648  bnj1098  34797  bnj1533  34866  bnj121  34884  bnj124  34885  bnj130  34888  bnj153  34894  bnj207  34895  bnj611  34932  bnj864  34936  bnj865  34937  bnj1000  34955  bnj978  34963  bnj1021  34980  bnj1047  34987  bnj1049  34988  bnj1090  34993  bnj1110  34996  bnj1128  35004  bnj1145  35007  bnj1171  35014  bnj1172  35015  bnj1174  35017  bnj1176  35019  bnj1280  35034  axinfprim  35706  dfon2lem9  35792  dffun10  35915  elicc3  36318  filnetlem4  36382  df3nandALT1  36400  df3nandALT2  36401  bj-ssbeq  36654  bj-ax12ssb  36659  pibt2  37418  poimirlem30  37657  inxpssidinxp  38317  cnvref5  38352  lcvnbtwn3  39029  isat3  39308  cdleme25cv  40360  cdlemefrs29bpre0  40398  cdlemk35  40914  dvrelogpow2b  42069  aks4d1p1p4  42072  aks6d1c2p2  42120  aks5lem3a  42190  aks5lem6  42193  unitscyglem2  42197  unitscyglem3  42198  metakunt6  42211  metakunt24  42229  2xp3dxp2ge1d  42242  sn-axrep5v  42255  supinf  42283  dford4  43041  ifpidg  43504  ifpid1g  43507  ifpim23g  43508  ifpororb  43518  ifpbibib  43523  elinintrab  43590  undmrnresiss  43617  cotrintab  43627  elintima  43666  frege60b  43918  frege91  43967  frege97  43973  frege98  43974  dffrege99  43975  frege109  43985  frege110  43986  frege131  44007  frege133  44009  ntrneiiso  44104  int-sqdefd  44194  int-sqgeq0d  44199  ismnuprim  44313  pm10.541  44386  pm13.196a  44433  2sbc6g  44434  expcomdg  44520  impexpd  44533  supxrleubrnmptf  45462  fsummulc1f  45586  fsumiunss  45590  fnlimfvre2  45692  limsupreuz  45752  lmbr3v  45760  dvmptmulf  45952  dvmptfprodlem  45959  sge0ltfirpmpt2  46441  hoidmv1le  46609  hoidmvle  46615  vonioolem2  46696  smflimlem3  46788  ldepslinc  48426  map0cor  48764  setrec1lem2  49207  setrec2  49214  sbidd-misc  49238