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  951  pm5.6  1002  nannan  1494  alimex  1829  19.36v  1987  2sb6  2086  sbrimvw  2091  sbal  2170  19.36  2231  sbn  2284  sbrim  2308  sblim  2310  sbnfOLD  2317  cbvsbvf  2369  sbhb  2529  dfmo  2599  eu1  2613  r2allem  3148  r19.21vOLD  3187  r3al  3203  r19.21t  3259  nfra2wOLD  3306  rspc2gv  3645  reu2  3747  reu8  3755  2reu5lem3  3779  rmoanim  3916  rmoanimALT  3917  dfdif3OLD  4141  ssconb  4165  ssin  4260  difin  4291  reldisj  4476  ssundif  4511  ralidmw  4531  ralidm  4535  reuprg0  4727  raldifsni  4820  pwpw0  4838  unissb  4963  unissbOLD  4964  moabex  5479  dffr2  5661  dffr2ALT  5662  dfepfr  5684  ssrel2  5809  dffr3  6129  opreu2reurex  6325  dffr4  6352  fncnv  6651  fun11  6652  dff13  7292  naddssim  8741  marypha2lem3  9506  dfsup2  9513  wemapsolem  9619  inf2  9692  axinf2  9709  aceq1  10186  aceq0  10187  kmlem14  10233  dfackm  10236  zfac  10529  ac6n  10554  zfcndrep  10683  zfcndac  10688  axgroth6  10897  axgroth4  10901  grothprim  10903  prime  12724  raluz2  12962  fsuppmapnn0ub  14046  mptnn0fsuppr  14050  brtrclfv  15051  rpnnen2lem12  16273  isprm2  16729  isprm4  16731  pgpfac1  20124  pgpfac  20128  isirred2  20447  isdomn5  20732  evl1maprhm  22404  pmatcollpw2lem  22804  isclo2  23117  lmres  23329  ist1-2  23376  is1stc2  23471  alexsubALTlem3  24078  itg2cn  25818  ellimc3  25934  plydivex  26357  vieta1  26372  dchrelbas2  27299  conway  27862  nmobndseqi  30811  nmobndseqiALT  30812  cvnbtwn3  32320  elat2  32372  inpr0  32560  ssrelf  32637  isarchi2  33165  archiabl  33178  islinds5  33360  1arithidom  33530  esumcvgre  34055  signstfvneq0  34549  hashreprin  34597  breprexp  34610  bnj1098  34759  bnj1533  34828  bnj121  34846  bnj124  34847  bnj130  34850  bnj153  34856  bnj207  34857  bnj611  34894  bnj864  34898  bnj865  34899  bnj1000  34917  bnj978  34925  bnj1021  34942  bnj1047  34949  bnj1049  34950  bnj1090  34955  bnj1110  34958  bnj1128  34966  bnj1145  34969  bnj1171  34976  bnj1172  34977  bnj1174  34979  bnj1176  34981  bnj1280  34996  axinfprim  35668  dfon2lem9  35755  dffun10  35878  elicc3  36283  filnetlem4  36347  df3nandALT1  36365  df3nandALT2  36366  bj-ssbeq  36619  bj-ax12ssb  36624  pibt2  37383  poimirlem30  37610  inxpssidinxp  38272  cnvref5  38307  lcvnbtwn3  38984  isat3  39263  cdleme25cv  40315  cdlemefrs29bpre0  40353  cdlemk35  40869  dvrelogpow2b  42025  aks4d1p1p4  42028  aks6d1c2p2  42076  aks5lem3a  42146  aks5lem6  42149  unitscyglem2  42153  unitscyglem3  42154  metakunt6  42167  metakunt24  42185  2xp3dxp2ge1d  42198  sn-axrep5v  42209  supinf  42237  dford4  42986  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  44263  pm10.541  44336  pm13.196a  44383  2sbc6g  44384  expcomdg  44471  impexpd  44484  supxrleubrnmptf  45366  fsummulc1f  45492  fsumiunss  45496  fnlimfvre2  45598  limsupreuz  45658  limsupvaluz2  45659  lmbr3v  45666  dvmptmulf  45858  dvmptfprodlem  45865  sge0ltfirpmpt2  46347  hoidmv1le  46515  hoidmvle  46521  vonioolem2  46602  smflimlem3  46694  ldepslinc  48238  map0cor  48568  setrec1lem2  48780  setrec2  48787  sbidd-misc  48811