Theorem imbi2i 336

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  iman  401  anidmdbi  565  pm5.32  573  pm4.14  807  nan  830  imimorb  952  pm5.6  1003  nannan  1493  alimex  1827  19.36v  1984  2sb6  2083  sbrimvw  2088  sbal  2166  19.36  2227  sbn  2278  sbrim  2302  sblim  2304  sbnfOLD  2311  cbvsbvf  2363  sbhb  2523  dfmo  2593  eu1  2607  r2allem  3139  r19.21vOLD  3178  r3al  3194  r19.21t  3250  nfra2wOLD  3297  rspc2gv  3631  reu2  3733  reu8  3741  2reu5lem3  3765  rmoanim  3902  rmoanimALT  3903  dfdif3OLD  4127  ssconb  4151  ssin  4246  difin  4277  reldisj  4458  ssundif  4493  ralidmw  4513  ralidm  4517  reuprg0  4706  raldifsni  4799  pwpw0  4817  unissb  4943  unissbOLD  4944  moabex  5469  dffr2  5649  dffr2ALT  5650  dfepfr  5672  ssrel2  5797  dffr3  6119  opreu2reurex  6315  dffr4  6342  fncnv  6640  fun11  6641  dff13  7274  naddssim  8721  marypha2lem3  9474  dfsup2  9481  wemapsolem  9587  inf2  9660  axinf2  9677  aceq1  10154  aceq0  10155  kmlem14  10201  dfackm  10204  zfac  10497  ac6n  10522  zfcndrep  10651  zfcndac  10656  axgroth6  10865  axgroth4  10869  grothprim  10871  prime  12696  raluz2  12936  fsuppmapnn0ub  14032  mptnn0fsuppr  14036  brtrclfv  15037  rpnnen2lem12  16257  isprm2  16715  isprm4  16717  pgpfac1  20114  pgpfac  20118  isirred2  20437  isdomn5  20726  evl1maprhm  22398  pmatcollpw2lem  22798  isclo2  23111  lmres  23323  ist1-2  23370  is1stc2  23465  alexsubALTlem3  24072  itg2cn  25812  ellimc3  25928  plydivex  26353  vieta1  26368  dchrelbas2  27295  conway  27858  nmobndseqi  30807  nmobndseqiALT  30808  cvnbtwn3  32316  elat2  32368  inpr0  32557  ssrelf  32634  isarchi2  33174  archiabl  33187  islinds5  33374  1arithidom  33544  esumcvgre  34071  signstfvneq0  34565  hashreprin  34613  breprexp  34626  bnj1098  34775  bnj1533  34844  bnj121  34862  bnj124  34863  bnj130  34866  bnj153  34872  bnj207  34873  bnj611  34910  bnj864  34914  bnj865  34915  bnj1000  34933  bnj978  34941  bnj1021  34958  bnj1047  34965  bnj1049  34966  bnj1090  34971  bnj1110  34974  bnj1128  34982  bnj1145  34985  bnj1171  34992  bnj1172  34993  bnj1174  34995  bnj1176  34997  bnj1280  35012  axinfprim  35685  dfon2lem9  35772  dffun10  35895  elicc3  36299  filnetlem4  36363  df3nandALT1  36381  df3nandALT2  36382  bj-ssbeq  36635  bj-ax12ssb  36640  pibt2  37399  poimirlem30  37636  inxpssidinxp  38297  cnvref5  38332  lcvnbtwn3  39009  isat3  39288  cdleme25cv  40340  cdlemefrs29bpre0  40378  cdlemk35  40894  dvrelogpow2b  42049  aks4d1p1p4  42052  aks6d1c2p2  42100  aks5lem3a  42170  aks5lem6  42173  unitscyglem2  42177  unitscyglem3  42178  metakunt6  42191  metakunt24  42209  2xp3dxp2ge1d  42222  sn-axrep5v  42233  supinf  42261  dford4  43017  ifpidg  43480  ifpid1g  43483  ifpim23g  43484  ifpororb  43494  ifpbibib  43499  elinintrab  43566  undmrnresiss  43593  cotrintab  43603  elintima  43642  frege60b  43894  frege91  43943  frege97  43949  frege98  43950  dffrege99  43951  frege109  43961  frege110  43962  frege131  43983  frege133  43985  ntrneiiso  44080  int-sqdefd  44170  int-sqgeq0d  44175  ismnuprim  44289  pm10.541  44362  pm13.196a  44409  2sbc6g  44410  expcomdg  44497  impexpd  44510  supxrleubrnmptf  45400  fsummulc1f  45526  fsumiunss  45530  fnlimfvre2  45632  limsupreuz  45692  lmbr3v  45700  dvmptmulf  45892  dvmptfprodlem  45899  sge0ltfirpmpt2  46381  hoidmv1le  46549  hoidmvle  46555  vonioolem2  46636  smflimlem3  46728  ldepslinc  48354  map0cor  48684  setrec1lem2  48918  setrec2  48925  sbidd-misc  48949