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  1498  alimex  1832  19.36v  1994  2sb6  2091  sbrimvw  2096  sbal  2174  19.36  2235  sbn  2284  sbrim  2308  sblim  2309  sbnfOLD  2316  cbvsbvf  2365  sbhb  2523  dfmo  2593  eu1  2607  r2allem  3121  r3al  3171  r19.21t  3227  rspc2gv  3583  reu2  3680  reu8  3688  2reu5lem3  3712  rmoanim  3841  rmoanimALT  3842  dfdif3OLD  4067  ssconb  4091  ssin  4188  difin  4221  reldisj  4402  ssundif  4437  ralidmw  4466  ralidm  4467  reuprg0  4656  raldifsni  4748  pwpw0  4766  unissb  4893  moabexOLD  5404  dffr2  5582  dffr2ALT  5583  dfepfr  5605  ssrel2  5731  dffr3  6055  opreu2reurex  6249  dffr4  6275  fncnv  6562  fun11  6563  dff13  7197  naddssim  8609  marypha2lem3  9332  dfsup2  9339  wemapsolem  9447  inf2  9524  axinf2  9541  aceq1  10019  aceq0  10020  kmlem14  10066  dfackm  10069  zfac  10362  ac6n  10387  zfcndrep  10516  zfcndac  10521  axgroth6  10730  axgroth4  10734  grothprim  10736  prime  12564  raluz2  12801  fsuppmapnn0ub  13909  mptnn0fsuppr  13913  brtrclfv  14916  rpnnen2lem12  16141  isprm2  16600  isprm4  16602  pgpfac1  20002  pgpfac  20006  isirred2  20348  isdomn5  20634  evl1maprhm  22314  pmatcollpw2lem  22712  isclo2  23023  lmres  23235  ist1-2  23282  is1stc2  23377  alexsubALTlem3  23984  itg2cn  25711  ellimc3  25827  plydivex  26252  vieta1  26267  dchrelbas2  27195  conway  27760  nmobndseqi  30780  nmobndseqiALT  30781  cvnbtwn3  32289  elat2  32341  inpr0  32533  ssrelf  32619  isarchi2  33195  archiabl  33208  islinds5  33376  1arithidom  33546  esumcvgre  34176  signstfvneq0  34657  hashreprin  34705  breprexp  34718  bnj1098  34867  bnj1533  34936  bnj121  34954  bnj124  34955  bnj130  34958  bnj153  34964  bnj207  34965  bnj611  35002  bnj864  35006  bnj865  35007  bnj1000  35025  bnj978  35033  bnj1021  35050  bnj1047  35057  bnj1049  35058  bnj1090  35063  bnj1110  35066  bnj1128  35074  bnj1145  35077  bnj1171  35084  bnj1172  35085  bnj1174  35087  bnj1176  35089  bnj1280  35104  axreg  35197  axregscl  35198  axinfprim  35822  dfon2lem9  35905  dffun10  36028  elicc3  36433  filnetlem4  36497  df3nandALT1  36515  df3nandALT2  36516  bj-ssbeq  36770  bj-ax12ssb  36775  pibt2  37534  poimirlem30  37763  inxpssidinxp  38427  cnvref5  38456  lcvnbtwn3  39200  isat3  39479  cdleme25cv  40530  cdlemefrs29bpre0  40568  cdlemk35  41084  dvrelogpow2b  42234  aks4d1p1p4  42237  aks6d1c2p2  42285  aks5lem3a  42355  aks5lem6  42358  unitscyglem2  42362  unitscyglem3  42363  sn-axrep5v  42387  supinf  42412  dford4  43186  ifpidg  43648  ifpid1g  43651  ifpim23g  43652  ifpororb  43662  ifpbibib  43667  elinintrab  43734  undmrnresiss  43761  cotrintab  43771  elintima  43810  frege60b  44062  frege91  44111  frege97  44117  frege98  44118  dffrege99  44119  frege109  44129  frege110  44130  frege131  44151  frege133  44153  ntrneiiso  44248  int-sqdefd  44338  int-sqgeq0d  44343  ismnuprim  44451  pm10.541  44524  pm13.196a  44571  2sbc6g  44572  expcomdg  44657  impexpd  44670  supxrleubrnmptf  45611  fsummulc1f  45733  fsumiunss  45737  fnlimfvre2  45837  limsupreuz  45897  lmbr3v  45905  dvmptmulf  46097  dvmptfprodlem  46104  sge0ltfirpmpt2  46586  hoidmv1le  46754  hoidmvle  46760  vonioolem2  46841  smflimlem3  46933  ldepslinc  48671  map0cor  49016  setrec1lem2  49849  setrec2  49856  sbidd-misc  49880