Theorem imbi2i 325

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  iman  439  pm4.14  600  nan  602  pm5.32  666  anidmdbi  676  imimorb  917  pm5.6  949  nannan  1443  alimex  1748  19.36v  1891  19.36  2085  sblim  2385  sban  2387  sbhb  2426  2sb6  2432  mo2v  2465  moabs  2489  eu1  2498  r2allem  2921  r3al  2924  r19.21t  2938  r19.21v  2943  ralbii  2963  r19.35  3065  reu2  3361  reu8  3369  2reu5lem3  3382  ssconb  3705  ssin  3797  difin  3823  reldisj  3972  ssundif  4004  raldifsni  4265  pwpw0  4284  pwsnALT  4367  unissb  4405  moabex  4854  dffr2  5003  dfepfr  5023  ssrelOLD  5131  ssrel2  5133  dffr3  5417  dffr4  5613  fncnv  5876  fun11  5877  dff13  6416  marypha2lem3  8226  dfsup2  8233  wemapsolem  8338  inf2  8403  axinf2  8420  aceq1  8823  aceq0  8824  kmlem14  8868  dfackm  8871  zfac  9165  ac6n  9190  zfcndrep  9315  zfcndac  9320  axgroth6  9529  axgroth4  9533  grothprim  9535  prime  11334  raluz2  11613  fsuppmapnn0ub  12657  mptnn0fsuppr  12661  brtrclfv  13591  rpnnen2lem12  14793  isprm2  15233  isprm4  15235  pgpfac1  18302  pgpfac  18306  isirred2  18524  pmatcollpw2lem  20401  isclo2  20702  lmres  20914  ist1-2  20961  is1stc2  21055  alexsubALTlem3  21663  itg2cn  23336  ellimc3  23449  plydivex  23856  vieta1  23871  dchrelbas2  24762  nmobndseqi  27018  nmobndseqiALT  27019  cvnbtwn3  28531  elat2  28583  ssrelf  28805  funcnvmptOLD  28850  isarchi2  29070  archiabl  29083  esumcvgre  29480  signstfvneq0  29975  bnj1098  30108  bnj1533  30176  bnj121  30194  bnj124  30195  bnj130  30198  bnj153  30204  bnj207  30205  bnj611  30242  bnj864  30246  bnj865  30247  bnj1000  30265  bnj978  30273  bnj1021  30288  bnj1047  30295  bnj1049  30296  bnj1090  30301  bnj1110  30304  bnj1128  30312  bnj1145  30315  bnj1171  30322  bnj1172  30323  bnj1174  30325  bnj1176  30327  bnj1280  30342  axinfprim  30837  dfon2lem9  30940  dffun10  31191  elicc3  31481  filnetlem4  31546  df3nandALT1  31566  df3nandALT2  31567  bj-ssbeq  31816  bj-ssb0  31817  bj-ax12ssb  31824  bj-ssbn  31830  bj-sbnf  32016  wl-nannan  32477  poimirlem30  32609  lcvnbtwn3  33333  isat3  33612  cdleme25cv  34664  cdlemefrs29bpre0  34702  cdlemk35  35218  dford4  36614  ifpidg  36855  ifpid1g  36858  ifpim23g  36859  ifpororb  36869  ifpbibib  36874  elinintrab  36902  undmrnresiss  36929  cotrintab  36940  elintima  36964  frege60b  37219  frege91  37268  frege97  37274  frege98  37275  dffrege99  37276  frege109  37286  frege110  37287  frege131  37308  frege133  37310  ntrneiiso  37409  int-rightdistd  37505  int-sqdefd  37506  int-sqgeq0d  37511  pm10.541  37588  pm13.196a  37637  2sbc6g  37638  expcomdg  37727  impexpd  37740  jcn  38228  fsummulc1f  38635  fsumiunss  38642  fnlimfvre2  38744  dvmptmulf  38827  dvmptfprodlem  38834  sge0ltfirpmpt2  39319  hoidmv1le  39484  hoidmvle  39490  vonioolem2  39572  smflimlem3  39659  rmoanim  39828  ldepslinc  42092  setrec1lem2  42234  setrec2  42241  sbidd-misc  42259