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  1497  alimex  1831  19.36v  1987  2sb6  2086  sbrimvw  2091  sbal  2169  19.36  2230  sbn  2280  sbrim  2304  sblim  2306  sbnfOLD  2313  cbvsbvf  2365  sbhb  2525  dfmo  2595  eu1  2609  r2allem  3128  r19.21vOLD  3166  r3al  3182  r19.21t  3236  rspc2gv  3611  reu2  3708  reu8  3716  2reu5lem3  3740  rmoanim  3869  rmoanimALT  3870  dfdif3OLD  4093  ssconb  4117  ssin  4214  difin  4247  reldisj  4428  ssundif  4463  ralidmw  4483  ralidm  4487  reuprg0  4678  raldifsni  4771  pwpw0  4789  unissb  4915  unissbOLD  4916  moabex  5434  dffr2  5615  dffr2ALT  5616  dfepfr  5638  ssrel2  5764  dffr3  6086  opreu2reurex  6283  dffr4  6309  fncnv  6608  fun11  6609  dff13  7246  naddssim  8695  marypha2lem3  9447  dfsup2  9454  wemapsolem  9562  inf2  9635  axinf2  9652  aceq1  10129  aceq0  10130  kmlem14  10176  dfackm  10179  zfac  10472  ac6n  10497  zfcndrep  10626  zfcndac  10631  axgroth6  10840  axgroth4  10844  grothprim  10846  prime  12672  raluz2  12911  fsuppmapnn0ub  14011  mptnn0fsuppr  14015  brtrclfv  15019  rpnnen2lem12  16241  isprm2  16699  isprm4  16701  pgpfac1  20061  pgpfac  20065  isirred2  20379  isdomn5  20668  evl1maprhm  22315  pmatcollpw2lem  22713  isclo2  23024  lmres  23236  ist1-2  23283  is1stc2  23378  alexsubALTlem3  23985  itg2cn  25714  ellimc3  25830  plydivex  26255  vieta1  26270  dchrelbas2  27198  conway  27761  nmobndseqi  30706  nmobndseqiALT  30707  cvnbtwn3  32215  elat2  32267  inpr0  32459  ssrelf  32541  isarchi2  33129  archiabl  33142  islinds5  33328  1arithidom  33498  esumcvgre  34068  signstfvneq0  34550  hashreprin  34598  breprexp  34611  bnj1098  34760  bnj1533  34829  bnj121  34847  bnj124  34848  bnj130  34851  bnj153  34857  bnj207  34858  bnj611  34895  bnj864  34899  bnj865  34900  bnj1000  34918  bnj978  34926  bnj1021  34943  bnj1047  34950  bnj1049  34951  bnj1090  34956  bnj1110  34959  bnj1128  34967  bnj1145  34970  bnj1171  34977  bnj1172  34978  bnj1174  34980  bnj1176  34982  bnj1280  34997  axinfprim  35669  dfon2lem9  35755  dffun10  35878  elicc3  36281  filnetlem4  36345  df3nandALT1  36363  df3nandALT2  36364  bj-ssbeq  36617  bj-ax12ssb  36622  pibt2  37381  poimirlem30  37620  inxpssidinxp  38280  cnvref5  38315  lcvnbtwn3  38992  isat3  39271  cdleme25cv  40323  cdlemefrs29bpre0  40361  cdlemk35  40877  dvrelogpow2b  42027  aks4d1p1p4  42030  aks6d1c2p2  42078  aks5lem3a  42148  aks5lem6  42151  unitscyglem2  42155  unitscyglem3  42156  metakunt6  42169  metakunt24  42187  2xp3dxp2ge1d  42200  sn-axrep5v  42213  supinf  42240  dford4  43000  ifpidg  43462  ifpid1g  43465  ifpim23g  43466  ifpororb  43476  ifpbibib  43481  elinintrab  43548  undmrnresiss  43575  cotrintab  43585  elintima  43624  frege60b  43876  frege91  43925  frege97  43931  frege98  43932  dffrege99  43933  frege109  43943  frege110  43944  frege131  43965  frege133  43967  ntrneiiso  44062  int-sqdefd  44152  int-sqgeq0d  44157  ismnuprim  44266  pm10.541  44339  pm13.196a  44386  2sbc6g  44387  expcomdg  44473  impexpd  44486  supxrleubrnmptf  45426  fsummulc1f  45548  fsumiunss  45552  fnlimfvre2  45654  limsupreuz  45714  lmbr3v  45722  dvmptmulf  45914  dvmptfprodlem  45921  sge0ltfirpmpt2  46403  hoidmv1le  46571  hoidmvle  46577  vonioolem2  46658  smflimlem3  46750  ldepslinc  48433  map0cor  48781  setrec1lem2  49500  setrec2  49507  sbidd-misc  49531