Theorem imbi2i 339

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  iman  406  anidmdbi  575  pm5.32  583  pm4.14  818  nan  842  imimorb  965  pm5.6  1017  nannan  1527  alimex  1861  19.36v  2023  2sb6  2120  sbrimvwOLD  2126  sbal  2204  19.36  2266  sbn  2315  sbrim  2339  sblim  2340  cbvsbvf  2395  sbhb  2553  dfmo2  2624  eu1  2638  r2allem  3153  r3al  3203  r19.21t  3259  rspc2gv  3591  reu2  3688  reu8  3696  2reu5lem3  3720  rmoanim  3848  rmoanimALT  3849  dfdif3OLD  4073  ssconb  4096  ssin  4191  difin  4225  reldisj  4413  ssundif  4448  ralidmw  4477  ralidm  4478  reuprg0  4668  raldifsni  4763  pwpw0  4779  unissb  4906  moabexOLD  5440  dffr2  5622  dffr2ALT  5623  dfepfr  5645  ssrel2  5771  dffr3  6101  opreu2reurex  6295  dffr4  6321  fncnv  6609  fun11  6610  dff13  7252  naddssim  8668  marypha2lem3  9393  dfsup2  9400  wemapsolem  9508  inf2  9588  axinf2  9605  aceq1  10097  aceq0  10098  kmlem14  10143  dfackm  10146  zfac  10439  ac6n  10464  zfcndrep  10594  zfcndac  10599  axgroth6  10808  axgroth4  10812  grothprim  10814  prime  12672  raluz2  12916  fsuppmapnn0ub  14027  mptnn0fsuppr  14031  brtrclfv  15035  rpnnen2lem12  16276  isprm2  16735  isprm4  16737  pgpfac1  20147  pgpfac  20151  isirred2  20499  isdomn5  20809  evl1maprhm  22539  pmatcollpw2lem  22934  isclo2  23245  lmres  23457  ist1-2  23504  is1stc2  23599  alexsubALTlem3  24206  itg2cn  25922  ellimc3  26038  plydivex  26458  vieta1  26473  dchrelbas2  27401  conway  27972  nmobndseqi  31131  nmobndseqiALT  31132  cvnbtwn3  32640  elat2  32692  inpr0  32878  ssrelf  32960  isarchi2  33505  archiabl  33518  islinds5  33682  1arithidom  33827  esumcvgre  34481  signstfvneq0  34959  hashreprin  35007  breprexp  35020  bnj1098  35172  bnj1533  35240  bnj121  35258  bnj124  35259  bnj130  35262  bnj153  35268  bnj207  35269  bnj611  35306  bnj864  35310  bnj865  35311  bnj1000  35329  bnj978  35337  bnj1021  35354  bnj1047  35361  bnj1049  35362  bnj1090  35367  bnj1110  35370  bnj1128  35378  bnj1145  35381  bnj1171  35388  bnj1172  35389  bnj1174  35391  bnj1176  35393  bnj1280  35408  axreg  35540  axregscl  35541  axinfprim  36198  dfon2lem9  36281  dffun10  36404  elicc3  36828  filnetlem4  36892  df3nandALT1  36910  df3nandALT2  36911  regsfromregtco  37049  regsfromunir1  37051  mh-infprim2bi  37058  bj-ssbeq  37275  bj-ax12ssb  37280  bj-alnnf  37362  qdiffALT  37972  pibt2  38063  poimirlem30  38301  inxpssidinxp  38971  cnvref5  39000  lcvnbtwn3  39802  isat3  40081  cdleme25cv  41132  cdlemefrs29bpre0  41170  cdlemk35  41686  dvrelogpow2b  42835  aks4d1p1p4  42838  aks6d1c2p2  42886  aks5lem3a  42956  aks5lem6  42959  unitscyglem2  42963  unitscyglem3  42964  sn-axrep5v  42988  supinf  43010  dford4  43756  ifpidg  44217  ifpid1g  44220  ifpim23g  44221  ifpororb  44231  ifpbibib  44236  elinintrab  44303  undmrnresiss  44330  cotrintab  44340  elintima  44379  frege60b  44631  frege91  44680  frege97  44686  frege98  44687  dffrege99  44688  frege109  44698  frege110  44699  frege131  44720  frege133  44722  ntrneiiso  44817  int-sqdefd  44907  int-sqgeq0d  44912  ismnuprim  45004  pm10.541  45077  pm13.196a  45124  2sbc6g  45125  expcomdg  45209  impexpd  45222  supxrleubrnmptf  46165  fsummulc1f  46287  fsumiunss  46291  fnlimfvre2  46391  limsupreuz  46451  lmbr3v  46459  dvmptmulf  46651  dvmptfprodlem  46658  sge0ltfirpmpt2  47140  hoidmv1le  47308  hoidmvle  47314  vonioolem2  47395  smflimlem3  47487  ldepslinc  49289  map0cor  49633  setrec1lem2  50466  setrec2  50473  sbidd-misc  50497