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  3621  reu2  3721  reu8  3729  2reu5lem3  3753  rmoanim  3888  rmoanimALT  3889  dfdif3  4114  ssconb  4137  ssin  4230  difin  4261  reldisj  4451  reldisjOLD  4452  ssundif  4487  ralidmw  4507  ralidm  4511  reuprg0  4706  raldifsni  4798  pwpw0  4816  pwsnOLD  4901  unissb  4943  unissbOLD  4944  moabex  5459  dffr2  5640  dffr2ALT  5641  dfepfr  5661  ssrel2  5784  dffr3  6096  opreu2reurex  6291  dffr4  6318  fncnv  6619  fun11  6620  dff13  7251  naddssim  8681  marypha2lem3  9429  dfsup2  9436  wemapsolem  9542  inf2  9615  axinf2  9632  aceq1  10109  aceq0  10110  kmlem14  10155  dfackm  10158  zfac  10452  ac6n  10477  zfcndrep  10606  zfcndac  10611  axgroth6  10820  axgroth4  10824  grothprim  10826  prime  12640  raluz2  12878  fsuppmapnn0ub  13957  mptnn0fsuppr  13961  brtrclfv  14946  rpnnen2lem12  16165  isprm2  16616  isprm4  16618  pgpfac1  19945  pgpfac  19949  isirred2  20228  isdomn5  20910  pmatcollpw2lem  22271  isclo2  22584  lmres  22796  ist1-2  22843  is1stc2  22938  alexsubALTlem3  23545  itg2cn  25273  ellimc3  25388  plydivex  25802  vieta1  25817  dchrelbas2  26730  conway  27290  nmobndseqi  30020  nmobndseqiALT  30021  cvnbtwn3  31529  elat2  31581  inpr0  31757  ssrelf  31832  isarchi2  32319  archiabl  32332  islinds5  32469  esumcvgre  33078  signstfvneq0  33572  hashreprin  33621  breprexp  33634  bnj1098  33783  bnj1533  33852  bnj121  33870  bnj124  33871  bnj130  33874  bnj153  33880  bnj207  33881  bnj611  33918  bnj864  33922  bnj865  33923  bnj1000  33941  bnj978  33949  bnj1021  33966  bnj1047  33973  bnj1049  33974  bnj1090  33979  bnj1110  33982  bnj1128  33990  bnj1145  33993  bnj1171  34000  bnj1172  34001  bnj1174  34003  bnj1176  34005  bnj1280  34020  axinfprim  34664  dfon2lem9  34752  dffun10  34875  elicc3  35191  filnetlem4  35255  df3nandALT1  35273  df3nandALT2  35274  bj-ssbeq  35519  bj-ax12ssb  35524  bj-sbnf  35708  pibt2  36287  poimirlem30  36507  inxpssidinxp  37174  cnvref5  37209  lcvnbtwn3  37887  isat3  38166  cdleme25cv  39218  cdlemefrs29bpre0  39256  cdlemk35  39772  dvrelogpow2b  40922  aks4d1p1p4  40925  aks6d1c2p2  40946  metakunt6  40979  metakunt24  40997  2xp3dxp2ge1d  41011  sn-axrep5v  41030  dford4  41754  ifpidg  42228  ifpid1g  42231  ifpim23g  42232  ifpororb  42242  ifpbibib  42247  elinintrab  42314  undmrnresiss  42341  cotrintab  42351  elintima  42390  frege60b  42642  frege91  42691  frege97  42697  frege98  42698  dffrege99  42699  frege109  42709  frege110  42710  frege131  42731  frege133  42733  ntrneiiso  42828  int-sqdefd  42919  int-sqgeq0d  42924  ismnuprim  43039  pm10.541  43112  pm13.196a  43159  2sbc6g  43160  expcomdg  43247  impexpd  43260  supxrleubrnmptf  44148  fsummulc1f  44274  fsumiunss  44278  fnlimfvre2  44380  limsupreuz  44440  limsupvaluz2  44441  lmbr3v  44448  dvmptmulf  44640  dvmptfprodlem  44647  sge0ltfirpmpt2  45129  hoidmv1le  45297  hoidmvle  45303  vonioolem2  45384  smflimlem3  45476  ldepslinc  47144  map0cor  47475  setrec1lem2  47687  setrec2  47694  sbidd-misc  47718