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  3122  r2allem  3125  r3al  3127  r19.21t  3139  nfra2wOLD  3154  moel  3357  rspc2gv  3570  reu2  3661  reu8  3669  2reu5lem3  3693  rmoanim  3828  rmoanimALT  3829  dfdif3  4050  ssconb  4073  ssin  4166  difin  4197  reldisj  4387  reldisjOLD  4388  ssundif  4420  ralidmw  4440  ralidm  4444  reuprg0  4640  raldifsni  4730  pwpw0  4748  pwsnOLD  4834  unissb  4875  moabex  5376  dffr2  5555  dffr2ALT  5556  dfepfr  5576  ssrel2  5698  dffr3  6009  opreu2reurex  6199  dffr4  6224  fncnv  6509  fun11  6510  dff13  7130  marypha2lem3  9194  dfsup2  9201  wemapsolem  9307  inf2  9379  axinf2  9396  aceq1  9871  aceq0  9872  kmlem14  9917  dfackm  9920  zfac  10214  ac6n  10239  zfcndrep  10368  zfcndac  10373  axgroth6  10582  axgroth4  10586  grothprim  10588  prime  12399  raluz2  12635  fsuppmapnn0ub  13713  mptnn0fsuppr  13717  brtrclfv  14711  rpnnen2lem12  15932  isprm2  16385  isprm4  16387  pgpfac1  19681  pgpfac  19685  isirred2  19941  pmatcollpw2lem  21924  isclo2  22237  lmres  22449  ist1-2  22496  is1stc2  22591  alexsubALTlem3  23198  itg2cn  24926  ellimc3  25041  plydivex  25455  vieta1  25470  dchrelbas2  26383  nmobndseqi  29138  nmobndseqiALT  29139  cvnbtwn3  30647  elat2  30699  inpr0  30877  ssrelf  30952  isarchi2  31436  archiabl  31449  islinds5  31560  esumcvgre  32056  signstfvneq0  32548  hashreprin  32597  breprexp  32610  bnj1098  32760  bnj1533  32829  bnj121  32847  bnj124  32848  bnj130  32851  bnj153  32857  bnj207  32858  bnj611  32895  bnj864  32899  bnj865  32900  bnj1000  32918  bnj978  32926  bnj1021  32943  bnj1047  32950  bnj1049  32951  bnj1090  32956  bnj1110  32959  bnj1128  32967  bnj1145  32970  bnj1171  32977  bnj1172  32978  bnj1174  32980  bnj1176  32982  bnj1280  32997  axinfprim  33644  dfon2lem9  33764  naddssim  33834  conway  33990  dffun10  34213  elicc3  34503  filnetlem4  34567  df3nandALT1  34585  df3nandALT2  34586  bj-ssbeq  34831  bj-ax12ssb  34836  bj-sbnf  35021  pibt2  35585  poimirlem30  35804  inxpssidinxp  36448  lcvnbtwn3  37039  isat3  37318  cdleme25cv  38369  cdlemefrs29bpre0  38407  cdlemk35  38923  dvrelogpow2b  40073  aks4d1p1p4  40076  metakunt6  40127  metakunt24  40145  2xp3dxp2ge1d  40159  isdomn5  40168  sn-axrep5v  40182  dford4  40848  ifpidg  41077  ifpid1g  41080  ifpim23g  41081  ifpororb  41091  ifpbibib  41096  elinintrab  41155  undmrnresiss  41182  cotrintab  41192  elintima  41231  frege60b  41483  frege91  41532  frege97  41538  frege98  41539  dffrege99  41540  frege109  41550  frege110  41551  frege131  41572  frege133  41574  ntrneiiso  41671  int-sqdefd  41762  int-sqgeq0d  41767  ismnuprim  41882  pm10.541  41955  pm13.196a  42002  2sbc6g  42003  expcomdg  42090  impexpd  42103  supxrleubrnmptf  42961  fsummulc1f  43082  fsumiunss  43086  fnlimfvre2  43188  limsupreuz  43248  limsupvaluz2  43249  lmbr3v  43256  dvmptmulf  43448  dvmptfprodlem  43455  sge0ltfirpmpt2  43934  hoidmv1le  44102  hoidmvle  44108  vonioolem2  44189  smflimlem3  44275  ldepslinc  45817  map0cor  46149  setrec1lem2  46361  setrec2  46368  sbidd-misc  46388