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  2361  sbhb  2519  dfmo  2589  eu1  2603  r2allem  3117  r3al  3167  r19.21t  3223  rspc2gv  3587  reu2  3685  reu8  3693  2reu5lem3  3717  rmoanim  3846  rmoanimALT  3847  dfdif3OLD  4069  ssconb  4093  ssin  4190  difin  4223  reldisj  4404  ssundif  4439  ralidmw  4459  ralidm  4463  reuprg0  4654  raldifsni  4746  pwpw0  4764  unissb  4890  moabex  5402  dffr2  5580  dffr2ALT  5581  dfepfr  5603  ssrel2  5728  dffr3  6050  opreu2reurex  6242  dffr4  6268  fncnv  6555  fun11  6556  dff13  7191  naddssim  8603  marypha2lem3  9327  dfsup2  9334  wemapsolem  9442  inf2  9519  axinf2  9536  aceq1  10011  aceq0  10012  kmlem14  10058  dfackm  10061  zfac  10354  ac6n  10379  zfcndrep  10508  zfcndac  10513  axgroth6  10722  axgroth4  10726  grothprim  10728  prime  12557  raluz2  12798  fsuppmapnn0ub  13902  mptnn0fsuppr  13906  brtrclfv  14909  rpnnen2lem12  16134  isprm2  16593  isprm4  16595  pgpfac1  19961  pgpfac  19965  isirred2  20306  isdomn5  20595  evl1maprhm  22264  pmatcollpw2lem  22662  isclo2  22973  lmres  23185  ist1-2  23232  is1stc2  23327  alexsubALTlem3  23934  itg2cn  25662  ellimc3  25778  plydivex  26203  vieta1  26218  dchrelbas2  27146  conway  27710  nmobndseqi  30723  nmobndseqiALT  30724  cvnbtwn3  32232  elat2  32284  inpr0  32476  ssrelf  32560  isarchi2  33127  archiabl  33140  islinds5  33304  1arithidom  33474  esumcvgre  34058  signstfvneq0  34540  hashreprin  34588  breprexp  34601  bnj1098  34750  bnj1533  34819  bnj121  34837  bnj124  34838  bnj130  34841  bnj153  34847  bnj207  34848  bnj611  34885  bnj864  34889  bnj865  34890  bnj1000  34908  bnj978  34916  bnj1021  34933  bnj1047  34940  bnj1049  34941  bnj1090  34946  bnj1110  34949  bnj1128  34957  bnj1145  34960  bnj1171  34967  bnj1172  34968  bnj1174  34970  bnj1176  34972  bnj1280  34987  axreg  35062  axregscl  35063  axinfprim  35679  dfon2lem9  35765  dffun10  35888  elicc3  36291  filnetlem4  36355  df3nandALT1  36373  df3nandALT2  36374  bj-ssbeq  36627  bj-ax12ssb  36632  pibt2  37391  poimirlem30  37630  inxpssidinxp  38290  cnvref5  38319  lcvnbtwn3  39007  isat3  39286  cdleme25cv  40337  cdlemefrs29bpre0  40375  cdlemk35  40891  dvrelogpow2b  42041  aks4d1p1p4  42044  aks6d1c2p2  42092  aks5lem3a  42162  aks5lem6  42165  unitscyglem2  42169  unitscyglem3  42170  sn-axrep5v  42189  supinf  42215  dford4  43002  ifpidg  43464  ifpid1g  43467  ifpim23g  43468  ifpororb  43478  ifpbibib  43483  elinintrab  43550  undmrnresiss  43577  cotrintab  43587  elintima  43626  frege60b  43878  frege91  43927  frege97  43933  frege98  43934  dffrege99  43935  frege109  43945  frege110  43946  frege131  43967  frege133  43969  ntrneiiso  44064  int-sqdefd  44154  int-sqgeq0d  44159  ismnuprim  44267  pm10.541  44340  pm13.196a  44387  2sbc6g  44388  expcomdg  44474  impexpd  44487  supxrleubrnmptf  45430  fsummulc1f  45552  fsumiunss  45556  fnlimfvre2  45658  limsupreuz  45718  lmbr3v  45726  dvmptmulf  45918  dvmptfprodlem  45925  sge0ltfirpmpt2  46407  hoidmv1le  46575  hoidmvle  46581  vonioolem2  46662  smflimlem3  46754  ldepslinc  48494  map0cor  48839  setrec1lem2  49673  setrec2  49680  sbidd-misc  49704