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  806  nan  829  imimorb  952  pm5.6  1003  nannan  1497  alimex  1831  19.36v  1993  2sb6  2087  sbrimvw  2092  sbal  2170  19.36  2231  sbn  2280  sbrim  2304  sblim  2305  sbnfOLD  2312  cbvsbvf  2362  sbhb  2520  dfmo  2590  eu1  2604  r2allem  3122  r19.21vOLD  3160  r3al  3176  r19.21t  3232  rspc2gv  3601  reu2  3699  reu8  3707  2reu5lem3  3731  rmoanim  3860  rmoanimALT  3861  dfdif3OLD  4084  ssconb  4108  ssin  4205  difin  4238  reldisj  4419  ssundif  4454  ralidmw  4474  ralidm  4478  reuprg0  4669  raldifsni  4762  pwpw0  4780  unissb  4906  unissbOLD  4907  moabex  5422  dffr2  5602  dffr2ALT  5603  dfepfr  5625  ssrel2  5751  dffr3  6073  opreu2reurex  6270  dffr4  6296  fncnv  6592  fun11  6593  dff13  7232  naddssim  8652  marypha2lem3  9395  dfsup2  9402  wemapsolem  9510  inf2  9583  axinf2  9600  aceq1  10077  aceq0  10078  kmlem14  10124  dfackm  10127  zfac  10420  ac6n  10445  zfcndrep  10574  zfcndac  10579  axgroth6  10788  axgroth4  10792  grothprim  10794  prime  12622  raluz2  12863  fsuppmapnn0ub  13967  mptnn0fsuppr  13971  brtrclfv  14975  rpnnen2lem12  16200  isprm2  16659  isprm4  16661  pgpfac1  20019  pgpfac  20023  isirred2  20337  isdomn5  20626  evl1maprhm  22273  pmatcollpw2lem  22671  isclo2  22982  lmres  23194  ist1-2  23241  is1stc2  23336  alexsubALTlem3  23943  itg2cn  25671  ellimc3  25787  plydivex  26212  vieta1  26227  dchrelbas2  27155  conway  27718  nmobndseqi  30715  nmobndseqiALT  30716  cvnbtwn3  32224  elat2  32276  inpr0  32468  ssrelf  32550  isarchi2  33146  archiabl  33159  islinds5  33345  1arithidom  33515  esumcvgre  34088  signstfvneq0  34570  hashreprin  34618  breprexp  34631  bnj1098  34780  bnj1533  34849  bnj121  34867  bnj124  34868  bnj130  34871  bnj153  34877  bnj207  34878  bnj611  34915  bnj864  34919  bnj865  34920  bnj1000  34938  bnj978  34946  bnj1021  34963  bnj1047  34970  bnj1049  34971  bnj1090  34976  bnj1110  34979  bnj1128  34987  bnj1145  34990  bnj1171  34997  bnj1172  34998  bnj1174  35000  bnj1176  35002  bnj1280  35017  axinfprim  35700  dfon2lem9  35786  dffun10  35909  elicc3  36312  filnetlem4  36376  df3nandALT1  36394  df3nandALT2  36395  bj-ssbeq  36648  bj-ax12ssb  36653  pibt2  37412  poimirlem30  37651  inxpssidinxp  38311  cnvref5  38340  lcvnbtwn3  39028  isat3  39307  cdleme25cv  40359  cdlemefrs29bpre0  40397  cdlemk35  40913  dvrelogpow2b  42063  aks4d1p1p4  42066  aks6d1c2p2  42114  aks5lem3a  42184  aks5lem6  42187  unitscyglem2  42191  unitscyglem3  42192  sn-axrep5v  42211  supinf  42237  dford4  43025  ifpidg  43487  ifpid1g  43490  ifpim23g  43491  ifpororb  43501  ifpbibib  43506  elinintrab  43573  undmrnresiss  43600  cotrintab  43610  elintima  43649  frege60b  43901  frege91  43950  frege97  43956  frege98  43957  dffrege99  43958  frege109  43968  frege110  43969  frege131  43990  frege133  43992  ntrneiiso  44087  int-sqdefd  44177  int-sqgeq0d  44182  ismnuprim  44290  pm10.541  44363  pm13.196a  44410  2sbc6g  44411  expcomdg  44497  impexpd  44510  supxrleubrnmptf  45454  fsummulc1f  45576  fsumiunss  45580  fnlimfvre2  45682  limsupreuz  45742  lmbr3v  45750  dvmptmulf  45942  dvmptfprodlem  45949  sge0ltfirpmpt2  46431  hoidmv1le  46599  hoidmvle  46605  vonioolem2  46686  smflimlem3  46778  ldepslinc  48502  map0cor  48847  setrec1lem2  49681  setrec2  49688  sbidd-misc  49712