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  807  nan  830  imimorb  953  pm5.6  1004  nannan  1499  alimex  1833  19.36v  1995  2sb6  2092  sbrimvw  2097  sbal  2175  19.36  2238  sbn  2287  sbrim  2311  sblim  2312  sbnfOLD  2319  cbvsbvf  2368  sbhb  2526  dfmo2  2597  eu1  2611  r2allem  3126  r3al  3176  r19.21t  3232  rspc2gv  3575  reu2  3672  reu8  3680  2reu5lem3  3704  rmoanim  3833  rmoanimALT  3834  dfdif3OLD  4059  ssconb  4083  ssin  4180  difin  4213  reldisj  4394  ssundif  4428  ralidmw  4457  ralidm  4458  reuprg0  4647  raldifsni  4739  pwpw0  4757  unissb  4884  moabexOLD  5406  dffr2  5585  dffr2ALT  5586  dfepfr  5608  ssrel2  5734  dffr3  6058  opreu2reurex  6252  dffr4  6278  fncnv  6565  fun11  6566  dff13  7202  naddssim  8614  marypha2lem3  9343  dfsup2  9350  wemapsolem  9458  inf2  9535  axinf2  9552  aceq1  10030  aceq0  10031  kmlem14  10077  dfackm  10080  zfac  10373  ac6n  10398  zfcndrep  10528  zfcndac  10533  axgroth6  10742  axgroth4  10746  grothprim  10748  prime  12601  raluz2  12838  fsuppmapnn0ub  13948  mptnn0fsuppr  13952  brtrclfv  14955  rpnnen2lem12  16183  isprm2  16642  isprm4  16644  pgpfac1  20048  pgpfac  20052  isirred2  20392  isdomn5  20678  evl1maprhm  22354  pmatcollpw2lem  22752  isclo2  23063  lmres  23275  ist1-2  23322  is1stc2  23417  alexsubALTlem3  24024  itg2cn  25740  ellimc3  25856  plydivex  26274  vieta1  26289  dchrelbas2  27214  conway  27785  nmobndseqi  30865  nmobndseqiALT  30866  cvnbtwn3  32374  elat2  32426  inpr0  32617  ssrelf  32703  isarchi2  33261  archiabl  33274  islinds5  33442  1arithidom  33612  esumcvgre  34251  signstfvneq0  34732  hashreprin  34780  breprexp  34793  bnj1098  34942  bnj1533  35010  bnj121  35028  bnj124  35029  bnj130  35032  bnj153  35038  bnj207  35039  bnj611  35076  bnj864  35080  bnj865  35081  bnj1000  35099  bnj978  35107  bnj1021  35124  bnj1047  35131  bnj1049  35132  bnj1090  35137  bnj1110  35140  bnj1128  35148  bnj1145  35151  bnj1171  35158  bnj1172  35159  bnj1174  35161  bnj1176  35163  bnj1280  35178  axreg  35287  axregscl  35288  axinfprim  35904  dfon2lem9  35987  dffun10  36110  elicc3  36515  filnetlem4  36579  df3nandALT1  36597  df3nandALT2  36598  regsfromregtco  36736  regsfromunir1  36738  mh-infprim2bi  36745  bj-ssbeq  36963  bj-ax12ssb  36968  bj-alnnf  37050  pibt2  37747  poimirlem30  37985  inxpssidinxp  38657  cnvref5  38686  lcvnbtwn3  39488  isat3  39767  cdleme25cv  40818  cdlemefrs29bpre0  40856  cdlemk35  41372  dvrelogpow2b  42521  aks4d1p1p4  42524  aks6d1c2p2  42572  aks5lem3a  42642  aks5lem6  42645  unitscyglem2  42649  unitscyglem3  42650  sn-axrep5v  42672  supinf  42695  dford4  43475  ifpidg  43936  ifpid1g  43939  ifpim23g  43940  ifpororb  43950  ifpbibib  43955  elinintrab  44022  undmrnresiss  44049  cotrintab  44059  elintima  44098  frege60b  44350  frege91  44399  frege97  44405  frege98  44406  dffrege99  44407  frege109  44417  frege110  44418  frege131  44439  frege133  44441  ntrneiiso  44536  int-sqdefd  44626  int-sqgeq0d  44631  ismnuprim  44739  pm10.541  44812  pm13.196a  44859  2sbc6g  44860  expcomdg  44945  impexpd  44958  supxrleubrnmptf  45897  fsummulc1f  46019  fsumiunss  46023  fnlimfvre2  46123  limsupreuz  46183  lmbr3v  46191  dvmptmulf  46383  dvmptfprodlem  46390  sge0ltfirpmpt2  46872  hoidmv1le  47040  hoidmvle  47046  vonioolem2  47127  smflimlem3  47219  ldepslinc  48997  map0cor  49342  setrec1lem2  50175  setrec2  50182  sbidd-misc  50206