Theorem imbi2i 338

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  jcndOLD  339  iman  404  anidmdbi  568  pm5.32  576  pm4.14  805  nan  827  imimorb  947  pm5.6  998  nannan  1487  alimex  1831  19.36v  1994  2sb6  2094  sbrimvlem  2101  sbal  2166  19.36  2232  sbn  2287  sbanOLD  2312  sblim  2315  sbanvOLD  2326  sbhb  2563  sbanALT  2610  dfmo  2682  eu1  2694  ralbii  3165  r19.21v  3175  r2allem  3200  r3al  3202  r19.21t  3214  rspc2gv  3632  reu2  3716  reu8  3724  2reu5lem3  3748  rmoanim  3878  rmoanimALT  3879  dfdif3  4091  ssconb  4114  ssin  4207  difin  4238  reldisj  4402  ssundif  4433  reuprg0  4638  raldifsni  4728  pwpw0  4746  pwsnOLD  4831  unissb  4870  moabex  5351  dffr2  5520  dfepfr  5540  ssrel2  5659  dffr3  5962  opreu2reurex  6145  dffr4  6164  fncnv  6427  fun11  6428  dff13  7013  marypha2lem3  8901  dfsup2  8908  wemapsolem  9014  inf2  9086  axinf2  9103  aceq1  9543  aceq0  9544  kmlem14  9589  dfackm  9592  zfac  9882  ac6n  9907  zfcndrep  10036  zfcndac  10041  axgroth6  10250  axgroth4  10254  grothprim  10256  prime  12064  raluz2  12298  fsuppmapnn0ub  13364  mptnn0fsuppr  13368  brtrclfv  14362  rpnnen2lem12  15578  isprm2  16026  isprm4  16028  pgpfac1  19202  pgpfac  19206  isirred2  19451  pmatcollpw2lem  21385  isclo2  21696  lmres  21908  ist1-2  21955  is1stc2  22050  alexsubALTlem3  22657  itg2cn  24364  ellimc3  24477  plydivex  24886  vieta1  24901  dchrelbas2  25813  nmobndseqi  28556  nmobndseqiALT  28557  cvnbtwn3  30065  elat2  30117  inpr0  30292  ssrelf  30366  isarchi2  30814  archiabl  30827  islinds5  30932  esumcvgre  31350  signstfvneq0  31842  hashreprin  31891  breprexp  31904  bnj1098  32055  bnj1533  32124  bnj121  32142  bnj124  32143  bnj130  32146  bnj153  32152  bnj207  32153  bnj611  32190  bnj864  32194  bnj865  32195  bnj1000  32213  bnj978  32221  bnj1021  32238  bnj1047  32245  bnj1049  32246  bnj1090  32251  bnj1110  32254  bnj1128  32262  bnj1145  32265  bnj1171  32272  bnj1172  32273  bnj1174  32275  bnj1176  32277  bnj1280  32292  axinfprim  32932  dfon2lem9  33036  conway  33264  dffun10  33375  elicc3  33665  filnetlem4  33729  df3nandALT1  33747  df3nandALT2  33748  bj-ssbeq  33986  bj-ax12ssb  33991  bj-sbnf  34164  pibt2  34701  wl-dfralsb  34852  wl-dfrexex  34865  wl-dfrexsb  34866  wl-dfrmosb  34868  poimirlem30  34937  inxpssidinxp  35588  lcvnbtwn3  36179  isat3  36458  cdleme25cv  37509  cdlemefrs29bpre0  37547  cdlemk35  38063  2xp3dxp2ge1d  39117  sn-axrep5v  39128  dford4  39646  ifpidg  39877  ifpid1g  39880  ifpim23g  39881  ifpororb  39891  ifpbibib  39896  elinintrab  39957  undmrnresiss  39984  cotrintab  39994  elintima  40018  frege60b  40271  frege91  40320  frege97  40326  frege98  40327  dffrege99  40328  frege109  40338  frege110  40339  frege131  40360  frege133  40362  ntrneiiso  40461  int-sqdefd  40554  int-sqgeq0d  40559  ismnuprim  40650  pm10.541  40719  pm13.196a  40766  2sbc6g  40767  expcomdg  40854  impexpd  40867  supxrleubrnmptf  41747  fsummulc1f  41871  fsumiunss  41876  fnlimfvre2  41978  limsupreuz  42038  limsupvaluz2  42039  lmbr3v  42046  dvmptmulf  42242  dvmptfprodlem  42249  sge0ltfirpmpt2  42728  hoidmv1le  42896  hoidmvle  42902  vonioolem2  42983  smflimlem3  43069  ldepslinc  44584  setrec1lem2  44811  setrec2  44818  sbidd-misc  44838