Theorem imbi2i 339

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 274	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  iman  406  anidmdbi  575  pm5.32  583  pm4.14  818  nan  842  imimorb  965  pm5.6  1017  nannan  1524  alimex  1858  19.36v  2020  2sb6  2126  sbrimvwOLD  2132  sbal  2210  19.36  2272  sbn  2321  sbrim  2345  sblim  2346  cbvsbvf  2401  sbhb  2559  dfmo2  2630  eu1  2644  r2allem  3159  r3al  3209  r19.21t  3265  rspc2gv  3600  reu2  3697  reu8  3705  2reu5lem3  3729  rmoanim  3856  rmoanimALT  3857  dfdif3OLD  4081  ssconb  4104  ssin  4199  difin  4233  reldisj  4416  ssundif  4450  ralidmw  4479  ralidm  4480  reuprg0  4670  raldifsni  4764  pwpw0  4780  unissb  4907  moabexOLD  5438  dffr2  5620  dffr2ALT  5621  dfepfr  5643  ssrel2  5769  dffr3  6099  opreu2reurex  6293  dffr4  6319  fncnv  6607  fun11  6608  dff13  7250  naddssim  8668  marypha2lem3  9393  dfsup2  9400  wemapsolem  9508  inf2  9588  axinf2  9605  aceq1  10097  aceq0  10098  kmlem14  10143  dfackm  10146  zfac  10440  ac6n  10465  zfcndrep  10595  zfcndac  10600  axgroth6  10809  axgroth4  10813  grothprim  10815  prime  12673  raluz2  12917  fsuppmapnn0ub  14027  mptnn0fsuppr  14031  brtrclfv  15035  rpnnen2lem12  16277  isprm2  16736  isprm4  16738  pgpfac1  20148  pgpfac  20152  isirred2  20499  isdomn5  20791  evl1maprhm  22504  pmatcollpw2lem  22899  isclo2  23210  lmres  23422  ist1-2  23469  is1stc2  23564  alexsubALTlem3  24171  itg2cn  25887  ellimc3  26003  plydivex  26423  vieta1  26438  dchrelbas2  27363  conway  27934  nmobndseqi  31068  nmobndseqiALT  31069  cvnbtwn3  32577  elat2  32629  inpr0  32815  ssrelf  32897  isarchi2  33442  archiabl  33455  islinds5  33621  1arithidom  33768  esumcvgre  34422  signstfvneq0  34900  hashreprin  34948  breprexp  34961  bnj1098  35113  bnj1533  35181  bnj121  35199  bnj124  35200  bnj130  35203  bnj153  35209  bnj207  35210  bnj611  35247  bnj864  35251  bnj865  35252  bnj1000  35270  bnj978  35278  bnj1021  35295  bnj1047  35302  bnj1049  35303  bnj1090  35308  bnj1110  35311  bnj1128  35319  bnj1145  35322  bnj1171  35329  bnj1172  35330  bnj1174  35332  bnj1176  35334  bnj1280  35349  axreg  35459  axregscl  35460  axinfprim  36093  dfon2lem9  36176  dffun10  36299  elicc3  36713  filnetlem4  36777  df3nandALT1  36795  df3nandALT2  36796  regsfromregtco  36934  regsfromunir1  36936  mh-infprim2bi  36943  bj-ssbeq  37160  bj-ax12ssb  37165  bj-alnnf  37247  qdiffALT  37855  pibt2  37946  poimirlem30  38184  inxpssidinxp  38856  cnvref5  38885  lcvnbtwn3  39687  isat3  39966  cdleme25cv  41017  cdlemefrs29bpre0  41055  cdlemk35  41571  dvrelogpow2b  42720  aks4d1p1p4  42723  aks6d1c2p2  42771  aks5lem3a  42841  aks5lem6  42844  unitscyglem2  42848  unitscyglem3  42849  sn-axrep5v  42873  supinf  42895  dford4  43643  ifpidg  44104  ifpid1g  44107  ifpim23g  44108  ifpororb  44118  ifpbibib  44123  elinintrab  44190  undmrnresiss  44217  cotrintab  44227  elintima  44266  frege60b  44518  frege91  44567  frege97  44573  frege98  44574  dffrege99  44575  frege109  44585  frege110  44586  frege131  44607  frege133  44609  ntrneiiso  44704  int-sqdefd  44794  int-sqgeq0d  44799  ismnuprim  44891  pm10.541  44964  pm13.196a  45011  2sbc6g  45012  expcomdg  45096  impexpd  45109  supxrleubrnmptf  46052  fsummulc1f  46174  fsumiunss  46178  fnlimfvre2  46278  limsupreuz  46338  lmbr3v  46346  dvmptmulf  46538  dvmptfprodlem  46545  sge0ltfirpmpt2  47027  hoidmv1le  47195  hoidmvle  47201  vonioolem2  47282  smflimlem3  47374  ldepslinc  49169  map0cor  49513  setrec1lem2  50346  setrec2  50353  sbidd-misc  50377