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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  iman  407  anidmdbi  576  pm5.32  584  pm4.14  819  nan  843  imimorb  965  pm5.6  1017  nannan  1526  alimex  1863  19.36v  2025  2sb6  2122  sbrimvwOLD  2128  sbal  2205  19.36  2266  sbn  2313  sbrim  2337  sblim  2338  cbvsbvf  2392  sbhb  2550  dfmo2  2621  eu1  2635  r2allem  3150  r3al  3200  r19.21t  3256  rspc2gv  3585  reu2  3682  reu8  3690  2reu5lem3  3714  rmoanim  3841  rmoanimALT  3842  ssconb  4078  ssin  4135  difin  4217  reldisj  4405  ssundif  4442  ralidmw  4471  ralidm  4472  reuprg0  4662  raldifsni  4757  pwpw0  4773  unissb  4900  moabexOLD  5426  dffr2  5611  dffr2ALT  5612  dfepfr  5634  ssrel2  5760  dffr3  6096  opreu2reurex  6297  dffr4  6323  fncnv  6613  fun11  6614  dff13  7258  naddssim  8695  marypha2lem3  9429  dfsup2  9436  wemapsolem  9544  inf2  9624  axinf2  9641  setrec1lem2  9967  setrec2  9977  aceq1  10196  aceq0  10197  kmlem14  10242  dfackm  10245  zfac  10538  ac6n  10563  zfcndrep  10699  zfcndac  10704  axgroth6  10913  axgroth4  10917  grothprim  10919  prime  12780  raluz2  13024  fsuppmapnn0ub  14138  mptnn0fsuppr  14142  brtrclfv  15155  rpnnen2lem12  16393  isprm2  16857  isprm4  16859  pgpfac1  20296  pgpfac  20300  isirred2  20651  isdomn5  20962  evl1maprhm  22697  pmatcollpw2lem  23095  isclo2  23406  lmres  23618  ist1-2  23665  is1stc2  23760  alexsubALTlem3  24368  itg2cn  26084  ellimc3  26199  plydivex  26618  vieta1  26635  dchrelbas2  27564  conway  28165  nmobndseqi  31381  nmobndseqiALT  31382  cvnbtwn3  32890  elat2  32942  inpr0  33128  ssrelf  33209  isarchi2  33746  archiabl  33759  islinds5  33923  1arithidom  34069  esumcvgre  34723  signstfvneq0  35201  hashreprin  35249  breprexp  35262  bnj1098  35414  bnj1533  35482  bnj121  35500  bnj124  35501  bnj130  35504  bnj153  35510  bnj207  35511  bnj611  35548  bnj864  35552  bnj865  35553  bnj1000  35571  bnj978  35579  bnj1021  35596  bnj1047  35603  bnj1049  35604  bnj1090  35609  bnj1110  35612  bnj1128  35620  bnj1145  35623  bnj1171  35630  bnj1172  35631  bnj1174  35633  bnj1176  35635  bnj1280  35650  axreg  35795  axregscl  35796  axinfprim  36471  dfon2lem9  36553  dffun10  36676  elicc3  37105  filnetlem4  37169  df3nandALT1  37187  df3nandALT2  37188  regsfromregtco  37326  regsfromunir1  37328  mh-infprim2bi  37335  bj-ssbeq  37552  bj-ax12ssb  37557  bj-alnnf  37639  qdiffALT  38250  pibt2  38341  poimirlem30  38569  inxpssidinxp  39255  cnvref5  39284  lcvnbtwn3  40086  isat3  40365  cdleme25cv  41416  cdlemefrs29bpre0  41454  cdlemk35  41970  dvrelogpow2b  43119  aks4d1p1p4  43122  aks6d1c2p2  43170  aks5lem3a  43240  aks5lem6  43243  unitscyglem2  43247  unitscyglem3  43248  sn-axrep5v  43272  supinf  43294  dford4  44036  ifpidg  44492  ifpid1g  44495  ifpim23g  44496  ifpororb  44506  ifpbibib  44511  elinintrab  44578  undmrnresiss  44604  cotrintab  44614  elintima  44653  frege60b  44905  frege91  44954  frege97  44960  frege98  44961  dffrege99  44962  frege109  44972  frege110  44973  frege131  44994  frege133  44996  ntrneiiso  45091  int-sqdefd  45181  int-sqgeq0d  45186  ismnuprim  45278  pm10.541  45351  pm13.196a  45398  2sbc6g  45399  expcomdg  45483  impexpd  45496  supxrleubrnmptf  46461  fsummulc1f  46583  fsumiunss  46587  fnlimfvre2  46687  limsupreuz  46747  lmbr3v  46755  dvmptmulf  46947  dvmptfprodlem  46954  sge0ltfirpmpt2  47436  hoidmv1le  47604  hoidmvle  47610  vonioolem2  47691  smflimlem3  47783  ldepslinc  49621  map0cor  49965  sbidd-misc  50812