Theorem imbi2i 338

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  jcndOLD  339  iman  404  anidmdbi  568  pm5.32  576  pm4.14  805  nan  827  imimorb  947  pm5.6  998  nannan  1486  alimex  1827  19.36v  1990  2sb6  2090  sbrimvlem  2097  sbal  2162  19.36  2228  sbn  2283  sbanOLD  2308  sblim  2311  sbanvOLD  2322  sbhb  2559  sbanALT  2606  dfmo  2678  eu1  2690  ralbii  3165  r19.21v  3175  r2allem  3200  r3al  3202  r19.21t  3214  rspc2gv  3631  reu2  3715  reu8  3723  2reu5lem3  3747  rmoanim  3877  rmoanimALT  3878  dfdif3  4090  ssconb  4113  ssin  4206  difin  4237  reldisj  4401  ssundif  4432  reuprg0  4631  raldifsni  4721  pwpw0  4739  pwsnALT  4824  unissb  4862  moabex  5343  dffr2  5514  dfepfr  5534  ssrel2  5653  dffr3  5956  opreu2reurex  6139  dffr4  6158  fncnv  6421  fun11  6422  dff13  7007  marypha2lem3  8895  dfsup2  8902  wemapsolem  9008  inf2  9080  axinf2  9097  aceq1  9537  aceq0  9538  kmlem14  9583  dfackm  9586  zfac  9876  ac6n  9901  zfcndrep  10030  zfcndac  10035  axgroth6  10244  axgroth4  10248  grothprim  10250  prime  12057  raluz2  12291  fsuppmapnn0ub  13357  mptnn0fsuppr  13361  brtrclfv  14356  rpnnen2lem12  15572  isprm2  16020  isprm4  16022  pgpfac1  19196  pgpfac  19200  isirred2  19445  pmatcollpw2lem  21379  isclo2  21690  lmres  21902  ist1-2  21949  is1stc2  22044  alexsubALTlem3  22651  itg2cn  24358  ellimc3  24471  plydivex  24880  vieta1  24895  dchrelbas2  25807  nmobndseqi  28550  nmobndseqiALT  28551  cvnbtwn3  30059  elat2  30111  inpr0  30286  ssrelf  30360  isarchi2  30809  archiabl  30822  islinds5  30927  esumcvgre  31345  signstfvneq0  31837  hashreprin  31886  breprexp  31899  bnj1098  32050  bnj1533  32119  bnj121  32137  bnj124  32138  bnj130  32141  bnj153  32147  bnj207  32148  bnj611  32185  bnj864  32189  bnj865  32190  bnj1000  32208  bnj978  32216  bnj1021  32233  bnj1047  32240  bnj1049  32241  bnj1090  32246  bnj1110  32249  bnj1128  32257  bnj1145  32260  bnj1171  32267  bnj1172  32268  bnj1174  32270  bnj1176  32272  bnj1280  32287  axinfprim  32927  dfon2lem9  33031  conway  33259  dffun10  33370  elicc3  33660  filnetlem4  33724  df3nandALT1  33742  df3nandALT2  33743  bj-ssbeq  33981  bj-ax12ssb  33986  bj-sbnf  34159  pibt2  34692  wl-dfralsb  34831  wl-dfrexex  34844  wl-dfrexsb  34845  wl-dfrmosb  34847  poimirlem30  34916  inxpssidinxp  35567  lcvnbtwn3  36158  isat3  36437  cdleme25cv  37488  cdlemefrs29bpre0  37526  cdlemk35  38042  sn-axrep5v  39101  dford4  39619  ifpidg  39850  ifpid1g  39853  ifpim23g  39854  ifpororb  39864  ifpbibib  39869  elinintrab  39930  undmrnresiss  39957  cotrintab  39967  elintima  39991  frege60b  40244  frege91  40293  frege97  40299  frege98  40300  dffrege99  40301  frege109  40311  frege110  40312  frege131  40333  frege133  40335  ntrneiiso  40434  int-sqdefd  40527  int-sqgeq0d  40532  ismnuprim  40623  pm10.541  40692  pm13.196a  40739  2sbc6g  40740  expcomdg  40827  impexpd  40840  supxrleubrnmptf  41720  fsummulc1f  41844  fsumiunss  41849  fnlimfvre2  41951  limsupreuz  42011  limsupvaluz2  42012  lmbr3v  42019  dvmptmulf  42215  dvmptfprodlem  42222  sge0ltfirpmpt2  42702  hoidmv1le  42870  hoidmvle  42876  vonioolem2  42957  smflimlem3  43043  ldepslinc  44558  setrec1lem2  44785  setrec2  44792  sbidd-misc  44812