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  3842  rmoanimALT  3843  ssconb  4077  ssin  4134  difin  4216  reldisj  4405  ssundif  4442  ralidmw  4471  ralidm  4472  reuprg0  4659  raldifsni  4754  pwpw0  4830  unissb  4900  moabexOLD  5426  dffr2  5611  dffr2ALT  5612  dfepfr  5634  ssrel2  5761  dffr3  6098  opreu2reurex  6299  dffr4  6325  fncnv  6616  fun11  6617  dff13  7260  naddssim  8700  marypha2lem3  9434  dfsup2  9441  wemapsolem  9549  inf2  9629  axinf2  9646  setrec1lem2  9972  setrec2  9982  aceq1  10201  aceq0  10202  kmlem14  10247  dfackm  10250  zfac  10543  ac6n  10568  zfcndrep  10704  zfcndac  10709  axgroth6  10918  axgroth4  10922  grothprim  10924  prime  12785  raluz2  13029  fsuppmapnn0ub  14143  mptnn0fsuppr  14147  brtrclfv  15162  rpnnen2lem12  16400  isprm2  16864  isprm4  16866  pgpfac1  20303  pgpfac  20307  isirred2  20658  isdomn5  20969  evl1maprhm  22704  pmatcollpw2lem  23102  isclo2  23413  lmres  23625  ist1-2  23672  is1stc2  23767  alexsubALTlem3  24375  itg2cn  26091  ellimc3  26206  plydivex  26625  vieta1  26642  dchrelbas2  27571  conway  28172  nmobndseqi  31388  nmobndseqiALT  31389  cvnbtwn3  32897  elat2  32949  inpr0  33177  ssrelf  33258  isarchi2  33794  archiabl  33807  islinds5  33971  1arithidom  34117  esumcvgre  34771  signstfvneq0  35249  hashreprin  35297  breprexp  35310  bnj1098  35462  bnj1533  35530  bnj121  35548  bnj124  35549  bnj130  35552  bnj153  35558  bnj207  35559  bnj611  35596  bnj864  35600  bnj865  35601  bnj1000  35619  bnj978  35627  bnj1021  35644  bnj1047  35651  bnj1049  35652  bnj1090  35657  bnj1110  35660  bnj1128  35668  bnj1145  35671  bnj1171  35678  bnj1172  35679  bnj1174  35681  bnj1176  35683  bnj1280  35698  axreg  35853  axregscl  35854  axinfprim  36565  dfon2lem9  36647  dffun10  36770  elicc3  37199  filnetlem4  37263  df3nandALT1  37281  df3nandALT2  37282  regsfromregtco  37420  regsfromunir1  37422  mh-infprim2bi  37429  bj-ssbeq  37646  bj-ax12ssb  37651  bj-alnnf  37733  qdiffALT  38356  pibt2  38447  poimirlem30  38675  inxpssidinxp  39361  cnvref5  39390  lcvnbtwn3  40192  isat3  40471  cdleme25cv  41522  cdlemefrs29bpre0  41560  cdlemk35  42076  dvrelogpow2b  43225  aks4d1p1p4  43228  aks6d1c2p2  43276  aks5lem3a  43346  aks5lem6  43349  unitscyglem2  43353  unitscyglem3  43354  sn-axrep5v  43378  supinf  43400  dford4  44143  ifpidg  44599  ifpid1g  44602  ifpim23g  44603  ifpororb  44613  ifpbibib  44618  elinintrab  44685  undmrnresiss  44711  cotrintab  44721  elintima  44760  frege60b  45012  frege91  45061  frege97  45067  frege98  45068  dffrege99  45069  frege109  45079  frege110  45080  frege131  45101  frege133  45103  ntrneiiso  45198  int-sqdefd  45288  int-sqgeq0d  45293  ismnuprim  45385  pm10.541  45458  pm13.196a  45505  2sbc6g  45506  expcomdg  45590  impexpd  45603  supxrleubrnmptf  46568  fsummulc1f  46690  fsumiunss  46694  fnlimfvre2  46794  limsupreuz  46854  lmbr3v  46862  dvmptmulf  47054  dvmptfprodlem  47061  sge0ltfirpmpt2  47543  hoidmv1le  47711  hoidmvle  47717  vonioolem2  47798  smflimlem3  47890  ldepslinc  49728  map0cor  50073  sbidd-misc  50994