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  2237  sbn  2286  sbrim  2310  sblim  2311  sbnfOLD  2318  cbvsbvf  2367  sbhb  2525  dfmo2  2596  eu1  2610  r2allem  3124  r3al  3174  r19.21t  3230  rspc2gv  3586  reu2  3683  reu8  3691  2reu5lem3  3715  rmoanim  3844  rmoanimALT  3845  dfdif3OLD  4070  ssconb  4094  ssin  4191  difin  4224  reldisj  4405  ssundif  4440  ralidmw  4469  ralidm  4470  reuprg0  4659  raldifsni  4751  pwpw0  4769  unissb  4896  moabexOLD  5407  dffr2  5585  dffr2ALT  5586  dfepfr  5608  ssrel2  5734  dffr3  6058  opreu2reurex  6252  dffr4  6278  fncnv  6565  fun11  6566  dff13  7200  naddssim  8613  marypha2lem3  9340  dfsup2  9347  wemapsolem  9455  inf2  9532  axinf2  9549  aceq1  10027  aceq0  10028  kmlem14  10074  dfackm  10077  zfac  10370  ac6n  10395  zfcndrep  10525  zfcndac  10530  axgroth6  10739  axgroth4  10743  grothprim  10745  prime  12573  raluz2  12810  fsuppmapnn0ub  13918  mptnn0fsuppr  13922  brtrclfv  14925  rpnnen2lem12  16150  isprm2  16609  isprm4  16611  pgpfac1  20011  pgpfac  20015  isirred2  20357  isdomn5  20643  evl1maprhm  22323  pmatcollpw2lem  22721  isclo2  23032  lmres  23244  ist1-2  23291  is1stc2  23386  alexsubALTlem3  23993  itg2cn  25720  ellimc3  25836  plydivex  26261  vieta1  26276  dchrelbas2  27204  conway  27775  nmobndseqi  30854  nmobndseqiALT  30855  cvnbtwn3  32363  elat2  32415  inpr0  32607  ssrelf  32693  isarchi2  33267  archiabl  33280  islinds5  33448  1arithidom  33618  esumcvgre  34248  signstfvneq0  34729  hashreprin  34777  breprexp  34790  bnj1098  34939  bnj1533  35008  bnj121  35026  bnj124  35027  bnj130  35030  bnj153  35036  bnj207  35037  bnj611  35074  bnj864  35078  bnj865  35079  bnj1000  35097  bnj978  35105  bnj1021  35122  bnj1047  35129  bnj1049  35130  bnj1090  35135  bnj1110  35138  bnj1128  35146  bnj1145  35149  bnj1171  35156  bnj1172  35157  bnj1174  35159  bnj1176  35161  bnj1280  35176  axreg  35283  axregscl  35284  axinfprim  35900  dfon2lem9  35983  dffun10  36106  elicc3  36511  filnetlem4  36575  df3nandALT1  36593  df3nandALT2  36594  regsfromregtr  36668  regsfromunir1  36670  bj-ssbeq  36854  bj-ax12ssb  36859  pibt2  37622  poimirlem30  37851  inxpssidinxp  38515  cnvref5  38544  lcvnbtwn3  39288  isat3  39567  cdleme25cv  40618  cdlemefrs29bpre0  40656  cdlemk35  41172  dvrelogpow2b  42322  aks4d1p1p4  42325  aks6d1c2p2  42373  aks5lem3a  42443  aks5lem6  42446  unitscyglem2  42450  unitscyglem3  42451  sn-axrep5v  42473  supinf  42497  dford4  43271  ifpidg  43732  ifpid1g  43735  ifpim23g  43736  ifpororb  43746  ifpbibib  43751  elinintrab  43818  undmrnresiss  43845  cotrintab  43855  elintima  43894  frege60b  44146  frege91  44195  frege97  44201  frege98  44202  dffrege99  44203  frege109  44213  frege110  44214  frege131  44235  frege133  44237  ntrneiiso  44332  int-sqdefd  44422  int-sqgeq0d  44427  ismnuprim  44535  pm10.541  44608  pm13.196a  44655  2sbc6g  44656  expcomdg  44741  impexpd  44754  supxrleubrnmptf  45695  fsummulc1f  45817  fsumiunss  45821  fnlimfvre2  45921  limsupreuz  45981  lmbr3v  45989  dvmptmulf  46181  dvmptfprodlem  46188  sge0ltfirpmpt2  46670  hoidmv1le  46838  hoidmvle  46844  vonioolem2  46925  smflimlem3  47017  ldepslinc  48755  map0cor  49100  setrec1lem2  49933  setrec2  49940  sbidd-misc  49964