Theorem imbi2i 337

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 272	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  iman  402  anidmdbi  570  pm5.32  578  pm4.14  812  nan  835  imimorb  958  pm5.6  1009  nannan  1504  alimex  1838  19.36v  2000  2sb6  2097  sbrimvw  2102  sbal  2180  19.36  2242  sbn  2291  sbrim  2315  sblim  2316  cbvsbvf  2371  sbhb  2529  dfmo2  2600  eu1  2614  r2allem  3127  r3al  3177  r19.21t  3233  rspc2gv  3570  reu2  3666  reu8  3674  2reu5lem3  3698  rmoanim  3826  rmoanimALT  3827  dfdif3OLD  4049  ssconb  4072  ssin  4167  difin  4200  reldisj  4381  ssundif  4415  ralidmw  4444  ralidm  4445  reuprg0  4634  raldifsni  4728  pwpw0  4744  unissb  4871  moabexOLD  5398  dffr2  5579  dffr2ALT  5580  dfepfr  5602  ssrel2  5728  dffr3  6051  opreu2reurex  6245  dffr4  6271  fncnv  6558  fun11  6559  dff13  7198  naddssim  8611  marypha2lem3  9340  dfsup2  9347  wemapsolem  9455  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  20682  evl1maprhm  22365  pmatcollpw2lem  22760  isclo2  23071  lmres  23283  ist1-2  23330  is1stc2  23425  alexsubALTlem3  24032  itg2cn  25748  ellimc3  25864  plydivex  26281  vieta1  26296  dchrelbas2  27218  conway  27789  nmobndseqi  30868  nmobndseqiALT  30869  cvnbtwn3  32377  elat2  32429  inpr0  32620  ssrelf  32707  isarchi2  33266  archiabl  33279  islinds5  33450  1arithidom  33620  esumcvgre  34275  signstfvneq0  34756  hashreprin  34804  breprexp  34817  bnj1098  34966  bnj1533  35034  bnj121  35052  bnj124  35053  bnj130  35056  bnj153  35062  bnj207  35063  bnj611  35100  bnj864  35104  bnj865  35105  bnj1000  35123  bnj978  35131  bnj1021  35148  bnj1047  35155  bnj1049  35156  bnj1090  35161  bnj1110  35164  bnj1128  35172  bnj1145  35175  bnj1171  35182  bnj1172  35183  bnj1174  35185  bnj1176  35187  bnj1280  35202  axreg  35308  axregscl  35309  axinfprim  35934  dfon2lem9  36017  dffun10  36140  elicc3  36545  filnetlem4  36609  df3nandALT1  36627  df3nandALT2  36628  regsfromregtco  36766  regsfromunir1  36768  mh-infprim2bi  36775  bj-ssbeq  36993  bj-ax12ssb  36998  bj-alnnf  37080  qdiffALT  37688  pibt2  37779  poimirlem30  38017  inxpssidinxp  38689  cnvref5  38718  lcvnbtwn3  39520  isat3  39799  cdleme25cv  40850  cdlemefrs29bpre0  40888  cdlemk35  41404  dvrelogpow2b  42553  aks4d1p1p4  42556  aks6d1c2p2  42604  aks5lem3a  42674  aks5lem6  42677  unitscyglem2  42681  unitscyglem3  42682  sn-axrep5v  42704  supinf  42726  dford4  43474  ifpidg  43935  ifpid1g  43938  ifpim23g  43939  ifpororb  43949  ifpbibib  43954  elinintrab  44021  undmrnresiss  44048  cotrintab  44058  elintima  44097  frege60b  44349  frege91  44398  frege97  44404  frege98  44405  dffrege99  44406  frege109  44416  frege110  44417  frege131  44438  frege133  44440  ntrneiiso  44535  int-sqdefd  44625  int-sqgeq0d  44630  ismnuprim  44738  pm10.541  44811  pm13.196a  44858  2sbc6g  44859  expcomdg  44944  impexpd  44957  supxrleubrnmptf  45894  fsummulc1f  46016  fsumiunss  46020  fnlimfvre2  46120  limsupreuz  46180  lmbr3v  46188  dvmptmulf  46380  dvmptfprodlem  46387  sge0ltfirpmpt2  46869  hoidmv1le  47037  hoidmvle  47043  vonioolem2  47124  smflimlem3  47216  ldepslinc  49000  map0cor  49345  setrec1lem2  50178  setrec2  50185  sbidd-misc  50209