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 270	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:  jcndOLD  337  iman  402  anidmdbi  566  pm5.32  574  pm4.14  804  nan  827  imimorb  948  pm5.6  999  nannan  1492  alimex  1833  19.36v  1991  2sb6  2089  sbrimvw  2094  sbal  2159  19.36  2223  sbn  2277  sbrim  2301  sblim  2303  sbievg  2361  sbhb  2525  dfmo  2596  eu1  2612  r19.21vOLD  3114  r2allem  3117  r3al  3119  r19.21t  3139  nfra2wOLD  3155  moel  3358  rspc2gv  3569  reu2  3660  reu8  3668  2reu5lem3  3692  rmoanim  3827  rmoanimALT  3828  dfdif3  4049  ssconb  4072  ssin  4164  difin  4195  reldisj  4385  reldisjOLD  4386  ssundif  4418  ralidmw  4438  ralidm  4442  reuprg0  4638  raldifsni  4728  pwpw0  4746  pwsnOLD  4832  unissb  4873  moabex  5374  dffr2  5553  dffr2ALT  5554  dfepfr  5574  ssrel2  5696  dffr3  6007  opreu2reurex  6197  dffr4  6222  fncnv  6507  fun11  6508  dff13  7128  marypha2lem3  9196  dfsup2  9203  wemapsolem  9309  inf2  9381  axinf2  9398  aceq1  9873  aceq0  9874  kmlem14  9919  dfackm  9922  zfac  10216  ac6n  10241  zfcndrep  10370  zfcndac  10375  axgroth6  10584  axgroth4  10588  grothprim  10590  prime  12401  raluz2  12637  fsuppmapnn0ub  13715  mptnn0fsuppr  13719  brtrclfv  14713  rpnnen2lem12  15934  isprm2  16387  isprm4  16389  pgpfac1  19683  pgpfac  19687  isirred2  19943  pmatcollpw2lem  21926  isclo2  22239  lmres  22451  ist1-2  22498  is1stc2  22593  alexsubALTlem3  23200  itg2cn  24928  ellimc3  25043  plydivex  25457  vieta1  25472  dchrelbas2  26385  nmobndseqi  29141  nmobndseqiALT  29142  cvnbtwn3  30650  elat2  30702  inpr0  30880  ssrelf  30955  isarchi2  31439  archiabl  31452  islinds5  31563  esumcvgre  32059  signstfvneq0  32551  hashreprin  32600  breprexp  32613  bnj1098  32763  bnj1533  32832  bnj121  32850  bnj124  32851  bnj130  32854  bnj153  32860  bnj207  32861  bnj611  32898  bnj864  32902  bnj865  32903  bnj1000  32921  bnj978  32929  bnj1021  32946  bnj1047  32953  bnj1049  32954  bnj1090  32959  bnj1110  32962  bnj1128  32970  bnj1145  32973  bnj1171  32980  bnj1172  32981  bnj1174  32983  bnj1176  32985  bnj1280  33000  axinfprim  33647  dfon2lem9  33767  naddssim  33837  conway  33993  dffun10  34216  elicc3  34506  filnetlem4  34570  df3nandALT1  34588  df3nandALT2  34589  bj-ssbeq  34834  bj-ax12ssb  34839  bj-sbnf  35024  pibt2  35588  poimirlem30  35807  inxpssidinxp  36451  lcvnbtwn3  37042  isat3  37321  cdleme25cv  38372  cdlemefrs29bpre0  38410  cdlemk35  38926  dvrelogpow2b  40076  aks4d1p1p4  40079  metakunt6  40130  metakunt24  40148  2xp3dxp2ge1d  40162  isdomn5  40171  sn-axrep5v  40185  dford4  40851  ifpidg  41098  ifpid1g  41101  ifpim23g  41102  ifpororb  41112  ifpbibib  41117  elinintrab  41185  undmrnresiss  41212  cotrintab  41222  elintima  41261  frege60b  41513  frege91  41562  frege97  41568  frege98  41569  dffrege99  41570  frege109  41580  frege110  41581  frege131  41602  frege133  41604  ntrneiiso  41701  int-sqdefd  41792  int-sqgeq0d  41797  ismnuprim  41912  pm10.541  41985  pm13.196a  42032  2sbc6g  42033  expcomdg  42120  impexpd  42133  supxrleubrnmptf  42991  fsummulc1f  43112  fsumiunss  43116  fnlimfvre2  43218  limsupreuz  43278  limsupvaluz2  43279  lmbr3v  43286  dvmptmulf  43478  dvmptfprodlem  43485  sge0ltfirpmpt2  43964  hoidmv1le  44132  hoidmvle  44138  vonioolem2  44219  smflimlem3  44308  ldepslinc  45850  map0cor  46182  setrec1lem2  46394  setrec2  46401  sbidd-misc  46421