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  1527  alimex  1864  19.36v  2026  2sb6  2123  sbrimvwOLD  2129  sbal  2206  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  3586  reu2  3683  reu8  3691  2reu5lem3  3715  rmoanim  3842  rmoanimALT  3843  ssconb  4089  ssin  4184  difin  4218  reldisj  4406  ssundif  4443  ralidmw  4472  ralidm  4473  reuprg0  4663  raldifsni  4758  pwpw0  4774  unissb  4901  moabexOLD  5434  dffr2  5616  dffr2ALT  5617  dfepfr  5639  ssrel2  5765  dffr3  6095  opreu2reurex  6292  dffr4  6318  fncnv  6606  fun11  6607  dff13  7251  naddssim  8674  marypha2lem3  9407  dfsup2  9414  wemapsolem  9522  inf2  9602  axinf2  9619  aceq1  10120  aceq0  10121  kmlem14  10166  dfackm  10169  zfac  10462  ac6n  10487  zfcndrep  10623  zfcndac  10628  axgroth6  10837  axgroth4  10841  grothprim  10843  prime  12702  raluz2  12946  fsuppmapnn0ub  14059  mptnn0fsuppr  14063  brtrclfv  15075  rpnnen2lem12  16313  isprm2  16772  isprm4  16774  pgpfac1  20209  pgpfac  20213  isirred2  20562  isdomn5  20872  evl1maprhm  22604  pmatcollpw2lem  23002  isclo2  23313  lmres  23525  ist1-2  23572  is1stc2  23667  alexsubALTlem3  24275  itg2cn  25991  ellimc3  26106  plydivex  26527  vieta1  26544  dchrelbas2  27473  conway  28044  nmobndseqi  31260  nmobndseqiALT  31261  cvnbtwn3  32769  elat2  32821  inpr0  33007  ssrelf  33088  isarchi2  33625  archiabl  33638  islinds5  33802  1arithidom  33947  esumcvgre  34601  signstfvneq0  35080  hashreprin  35128  breprexp  35141  bnj1098  35293  bnj1533  35361  bnj121  35379  bnj124  35380  bnj130  35383  bnj153  35389  bnj207  35390  bnj611  35427  bnj864  35431  bnj865  35432  bnj1000  35450  bnj978  35458  bnj1021  35475  bnj1047  35482  bnj1049  35483  bnj1090  35488  bnj1110  35491  bnj1128  35499  bnj1145  35502  bnj1171  35509  bnj1172  35510  bnj1174  35512  bnj1176  35514  bnj1280  35529  axreg  35653  axregscl  35654  axinfprim  36285  dfon2lem9  36368  dffun10  36491  elicc3  36936  filnetlem4  37000  df3nandALT1  37018  df3nandALT2  37019  regsfromregtco  37157  regsfromunir1  37159  mh-infprim2bi  37166  bj-ssbeq  37383  bj-ax12ssb  37388  bj-alnnf  37470  qdiffALT  38080  pibt2  38171  poimirlem30  38399  inxpssidinxp  39070  cnvref5  39099  lcvnbtwn3  39901  isat3  40180  cdleme25cv  41231  cdlemefrs29bpre0  41269  cdlemk35  41785  dvrelogpow2b  42934  aks4d1p1p4  42937  aks6d1c2p2  42985  aks5lem3a  43055  aks5lem6  43058  unitscyglem2  43062  unitscyglem3  43063  sn-axrep5v  43087  supinf  43109  dford4  43870  ifpidg  44331  ifpid1g  44334  ifpim23g  44335  ifpororb  44345  ifpbibib  44350  elinintrab  44417  undmrnresiss  44444  cotrintab  44454  elintima  44493  frege60b  44745  frege91  44794  frege97  44800  frege98  44801  dffrege99  44802  frege109  44812  frege110  44813  frege131  44834  frege133  44836  ntrneiiso  44931  int-sqdefd  45021  int-sqgeq0d  45026  ismnuprim  45118  pm10.541  45191  pm13.196a  45238  2sbc6g  45239  expcomdg  45323  impexpd  45336  supxrleubrnmptf  46279  fsummulc1f  46401  fsumiunss  46405  fnlimfvre2  46505  limsupreuz  46565  lmbr3v  46573  dvmptmulf  46765  dvmptfprodlem  46772  sge0ltfirpmpt2  47254  hoidmv1le  47422  hoidmvle  47428  vonioolem2  47509  smflimlem3  47601  ldepslinc  49439  map0cor  49783  setrec1lem2  50614  setrec2  50621  sbidd-misc  50645