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  807  nan  830  imimorb  953  pm5.6  1004  nannan  1499  alimex  1833  19.36v  1995  2sb6  2092  sbrimvw  2097  sbal  2175  19.36  2238  sbn  2287  sbrim  2311  sblim  2312  sbnfOLD  2319  cbvsbvf  2368  sbhb  2526  dfmo2  2597  eu1  2611  r2allem  3126  r3al  3176  r19.21t  3232  rspc2gv  3588  reu2  3685  reu8  3693  2reu5lem3  3717  rmoanim  3846  rmoanimALT  3847  dfdif3OLD  4072  ssconb  4096  ssin  4193  difin  4226  reldisj  4407  ssundif  4442  ralidmw  4471  ralidm  4472  reuprg0  4661  raldifsni  4753  pwpw0  4771  unissb  4898  moabexOLD  5414  dffr2  5593  dffr2ALT  5594  dfepfr  5616  ssrel2  5742  dffr3  6066  opreu2reurex  6260  dffr4  6286  fncnv  6573  fun11  6574  dff13  7210  naddssim  8623  marypha2lem3  9352  dfsup2  9359  wemapsolem  9467  inf2  9544  axinf2  9561  aceq1  10039  aceq0  10040  kmlem14  10086  dfackm  10089  zfac  10382  ac6n  10407  zfcndrep  10537  zfcndac  10542  axgroth6  10751  axgroth4  10755  grothprim  10757  prime  12585  raluz2  12822  fsuppmapnn0ub  13930  mptnn0fsuppr  13934  brtrclfv  14937  rpnnen2lem12  16162  isprm2  16621  isprm4  16623  pgpfac1  20023  pgpfac  20027  isirred2  20369  isdomn5  20655  evl1maprhm  22335  pmatcollpw2lem  22733  isclo2  23044  lmres  23256  ist1-2  23303  is1stc2  23398  alexsubALTlem3  24005  itg2cn  25732  ellimc3  25848  plydivex  26273  vieta1  26288  dchrelbas2  27216  conway  27787  nmobndseqi  30867  nmobndseqiALT  30868  cvnbtwn3  32376  elat2  32428  inpr0  32619  ssrelf  32705  isarchi2  33279  archiabl  33292  islinds5  33460  1arithidom  33630  esumcvgre  34269  signstfvneq0  34750  hashreprin  34798  breprexp  34811  bnj1098  34960  bnj1533  35028  bnj121  35046  bnj124  35047  bnj130  35050  bnj153  35056  bnj207  35057  bnj611  35094  bnj864  35098  bnj865  35099  bnj1000  35117  bnj978  35125  bnj1021  35142  bnj1047  35149  bnj1049  35150  bnj1090  35155  bnj1110  35158  bnj1128  35166  bnj1145  35169  bnj1171  35176  bnj1172  35177  bnj1174  35179  bnj1176  35181  bnj1280  35196  axreg  35305  axregscl  35306  axinfprim  35922  dfon2lem9  36005  dffun10  36128  elicc3  36533  filnetlem4  36597  df3nandALT1  36615  df3nandALT2  36616  regsfromregtr  36690  regsfromunir1  36692  bj-ssbeq  36898  bj-ax12ssb  36903  bj-alnnf  36980  pibt2  37672  poimirlem30  37901  inxpssidinxp  38573  cnvref5  38602  lcvnbtwn3  39404  isat3  39683  cdleme25cv  40734  cdlemefrs29bpre0  40772  cdlemk35  41288  dvrelogpow2b  42438  aks4d1p1p4  42441  aks6d1c2p2  42489  aks5lem3a  42559  aks5lem6  42562  unitscyglem2  42566  unitscyglem3  42567  sn-axrep5v  42589  supinf  42612  dford4  43386  ifpidg  43847  ifpid1g  43850  ifpim23g  43851  ifpororb  43861  ifpbibib  43866  elinintrab  43933  undmrnresiss  43960  cotrintab  43970  elintima  44009  frege60b  44261  frege91  44310  frege97  44316  frege98  44317  dffrege99  44318  frege109  44328  frege110  44329  frege131  44350  frege133  44352  ntrneiiso  44447  int-sqdefd  44537  int-sqgeq0d  44542  ismnuprim  44650  pm10.541  44723  pm13.196a  44770  2sbc6g  44771  expcomdg  44856  impexpd  44869  supxrleubrnmptf  45809  fsummulc1f  45931  fsumiunss  45935  fnlimfvre2  46035  limsupreuz  46095  lmbr3v  46103  dvmptmulf  46295  dvmptfprodlem  46302  sge0ltfirpmpt2  46784  hoidmv1le  46952  hoidmvle  46958  vonioolem2  47039  smflimlem3  47131  ldepslinc  48869  map0cor  49214  setrec1lem2  50047  setrec2  50054  sbidd-misc  50078