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 205

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 206

This theorem is referenced by:  jcndOLD  337  iman  403  anidmdbi  567  pm5.32  575  pm4.14  806  nan  829  imimorb  950  pm5.6  1001  nannan  1496  alimex  1834  19.36v  1992  2sb6  2090  sbrimvw  2095  sbal  2160  19.36  2224  sbn  2277  sbrim  2301  sblim  2303  cbvsbvf  2361  sbhb  2521  dfmo  2591  eu1  2607  r2allem  3143  r19.21vOLD  3181  r3al  3197  r19.21t  3251  nfra2wOLD  3298  rspc2gv  3622  reu2  3722  reu8  3730  2reu5lem3  3754  rmoanim  3889  rmoanimALT  3890  dfdif3  4115  ssconb  4138  ssin  4231  difin  4262  reldisj  4452  reldisjOLD  4453  ssundif  4488  ralidmw  4508  ralidm  4512  reuprg0  4707  raldifsni  4799  pwpw0  4817  pwsnOLD  4902  unissb  4944  unissbOLD  4945  moabex  5460  dffr2  5641  dffr2ALT  5642  dfepfr  5662  ssrel2  5786  dffr3  6099  opreu2reurex  6294  dffr4  6321  fncnv  6622  fun11  6623  dff13  7254  naddssim  8684  marypha2lem3  9432  dfsup2  9439  wemapsolem  9545  inf2  9618  axinf2  9635  aceq1  10112  aceq0  10113  kmlem14  10158  dfackm  10161  zfac  10455  ac6n  10480  zfcndrep  10609  zfcndac  10614  axgroth6  10823  axgroth4  10827  grothprim  10829  prime  12643  raluz2  12881  fsuppmapnn0ub  13960  mptnn0fsuppr  13964  brtrclfv  14949  rpnnen2lem12  16168  isprm2  16619  isprm4  16621  pgpfac1  19950  pgpfac  19954  isirred2  20235  isdomn5  20917  pmatcollpw2lem  22279  isclo2  22592  lmres  22804  ist1-2  22851  is1stc2  22946  alexsubALTlem3  23553  itg2cn  25281  ellimc3  25396  plydivex  25810  vieta1  25825  dchrelbas2  26740  conway  27300  nmobndseqi  30032  nmobndseqiALT  30033  cvnbtwn3  31541  elat2  31593  inpr0  31769  ssrelf  31844  isarchi2  32331  archiabl  32344  islinds5  32480  esumcvgre  33089  signstfvneq0  33583  hashreprin  33632  breprexp  33645  bnj1098  33794  bnj1533  33863  bnj121  33881  bnj124  33882  bnj130  33885  bnj153  33891  bnj207  33892  bnj611  33929  bnj864  33933  bnj865  33934  bnj1000  33952  bnj978  33960  bnj1021  33977  bnj1047  33984  bnj1049  33985  bnj1090  33990  bnj1110  33993  bnj1128  34001  bnj1145  34004  bnj1171  34011  bnj1172  34012  bnj1174  34014  bnj1176  34016  bnj1280  34031  axinfprim  34675  dfon2lem9  34763  dffun10  34886  elicc3  35202  filnetlem4  35266  df3nandALT1  35284  df3nandALT2  35285  bj-ssbeq  35530  bj-ax12ssb  35535  bj-sbnf  35719  pibt2  36298  poimirlem30  36518  inxpssidinxp  37185  cnvref5  37220  lcvnbtwn3  37898  isat3  38177  cdleme25cv  39229  cdlemefrs29bpre0  39267  cdlemk35  39783  dvrelogpow2b  40933  aks4d1p1p4  40936  aks6d1c2p2  40957  metakunt6  40990  metakunt24  41008  2xp3dxp2ge1d  41022  sn-axrep5v  41033  dford4  41768  ifpidg  42242  ifpid1g  42245  ifpim23g  42246  ifpororb  42256  ifpbibib  42261  elinintrab  42328  undmrnresiss  42355  cotrintab  42365  elintima  42404  frege60b  42656  frege91  42705  frege97  42711  frege98  42712  dffrege99  42713  frege109  42723  frege110  42724  frege131  42745  frege133  42747  ntrneiiso  42842  int-sqdefd  42933  int-sqgeq0d  42938  ismnuprim  43053  pm10.541  43126  pm13.196a  43173  2sbc6g  43174  expcomdg  43261  impexpd  43274  supxrleubrnmptf  44161  fsummulc1f  44287  fsumiunss  44291  fnlimfvre2  44393  limsupreuz  44453  limsupvaluz2  44454  lmbr3v  44461  dvmptmulf  44653  dvmptfprodlem  44660  sge0ltfirpmpt2  45142  hoidmv1le  45310  hoidmvle  45316  vonioolem2  45397  smflimlem3  45489  ldepslinc  47190  map0cor  47521  setrec1lem2  47733  setrec2  47740  sbidd-misc  47764