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 205

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 206

This theorem is referenced by:  iman  401  anidmdbi  565  pm5.32  573  pm4.14  804  nan  827  imimorb  948  pm5.6  999  nannan  1494  alimex  1832  19.36v  1990  2sb6  2088  sbrimvw  2093  sbal  2158  19.36  2222  sbn  2275  sbrim  2299  sblim  2301  cbvsbvf  2359  sbhb  2519  dfmo  2589  eu1  2605  r2allem  3141  r19.21vOLD  3179  r3al  3195  r19.21t  3249  nfra2wOLD  3296  rspc2gv  3621  reu2  3721  reu8  3729  2reu5lem3  3753  rmoanim  3888  rmoanimALT  3889  dfdif3  4114  ssconb  4137  ssin  4230  difin  4261  reldisj  4451  reldisjOLD  4452  ssundif  4487  ralidmw  4507  ralidm  4511  reuprg0  4706  raldifsni  4798  pwpw0  4816  pwsnOLD  4901  unissb  4943  unissbOLD  4944  moabex  5459  dffr2  5640  dffr2ALT  5641  dfepfr  5661  ssrel2  5785  dffr3  6098  opreu2reurex  6293  dffr4  6320  fncnv  6621  fun11  6622  dff13  7257  naddssim  8690  marypha2lem3  9438  dfsup2  9445  wemapsolem  9551  inf2  9624  axinf2  9641  aceq1  10118  aceq0  10119  kmlem14  10164  dfackm  10167  zfac  10461  ac6n  10486  zfcndrep  10615  zfcndac  10620  axgroth6  10829  axgroth4  10833  grothprim  10835  prime  12650  raluz2  12888  fsuppmapnn0ub  13967  mptnn0fsuppr  13971  brtrclfv  14956  rpnnen2lem12  16175  isprm2  16626  isprm4  16628  pgpfac1  19998  pgpfac  20002  isirred2  20319  isdomn5  21206  pmatcollpw2lem  22599  isclo2  22912  lmres  23124  ist1-2  23171  is1stc2  23266  alexsubALTlem3  23873  itg2cn  25613  ellimc3  25728  plydivex  26149  vieta1  26164  dchrelbas2  27083  conway  27645  nmobndseqi  30465  nmobndseqiALT  30466  cvnbtwn3  31974  elat2  32026  inpr0  32202  ssrelf  32277  isarchi2  32767  archiabl  32780  islinds5  32920  esumcvgre  33553  signstfvneq0  34047  hashreprin  34096  breprexp  34109  bnj1098  34258  bnj1533  34327  bnj121  34345  bnj124  34346  bnj130  34349  bnj153  34355  bnj207  34356  bnj611  34393  bnj864  34397  bnj865  34398  bnj1000  34416  bnj978  34424  bnj1021  34441  bnj1047  34448  bnj1049  34449  bnj1090  34454  bnj1110  34457  bnj1128  34465  bnj1145  34468  bnj1171  34475  bnj1172  34476  bnj1174  34478  bnj1176  34480  bnj1280  34495  axinfprim  35145  dfon2lem9  35233  dffun10  35356  elicc3  35666  filnetlem4  35730  df3nandALT1  35748  df3nandALT2  35749  bj-ssbeq  35994  bj-ax12ssb  35999  bj-sbnf  36183  pibt2  36762  poimirlem30  36982  inxpssidinxp  37649  cnvref5  37684  lcvnbtwn3  38362  isat3  38641  cdleme25cv  39693  cdlemefrs29bpre0  39731  cdlemk35  40247  dvrelogpow2b  41400  aks4d1p1p4  41403  aks6d1c2p2  41424  metakunt6  41457  metakunt24  41475  2xp3dxp2ge1d  41489  sn-axrep5v  41500  dford4  42231  ifpidg  42705  ifpid1g  42708  ifpim23g  42709  ifpororb  42719  ifpbibib  42724  elinintrab  42791  undmrnresiss  42818  cotrintab  42828  elintima  42867  frege60b  43119  frege91  43168  frege97  43174  frege98  43175  dffrege99  43176  frege109  43186  frege110  43187  frege131  43208  frege133  43210  ntrneiiso  43305  int-sqdefd  43396  int-sqgeq0d  43401  ismnuprim  43516  pm10.541  43589  pm13.196a  43636  2sbc6g  43637  expcomdg  43724  impexpd  43737  supxrleubrnmptf  44620  fsummulc1f  44746  fsumiunss  44750  fnlimfvre2  44852  limsupreuz  44912  limsupvaluz2  44913  lmbr3v  44920  dvmptmulf  45112  dvmptfprodlem  45119  sge0ltfirpmpt2  45601  hoidmv1le  45769  hoidmvle  45775  vonioolem2  45856  smflimlem3  45948  ldepslinc  47352  map0cor  47683  setrec1lem2  47895  setrec2  47902  sbidd-misc  47926