Theorem imbi2i 338

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 273	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  iman  405  anidmdbi  573  pm5.32  581  pm4.14  816  nan  840  imimorb  963  pm5.6  1014  nannan  1516  alimex  1850  19.36v  2012  2sb6  2118  sbrimvwOLD  2124  sbal  2202  19.36  2264  sbn  2313  sbrim  2337  sblim  2338  cbvsbvf  2393  sbhb  2551  dfmo2  2622  eu1  2636  r2allem  3149  r3al  3199  r19.21t  3255  rspc2gv  3590  reu2  3686  reu8  3694  2reu5lem3  3718  rmoanim  3845  rmoanimALT  3846  dfdif3OLD  4070  ssconb  4093  ssin  4188  difin  4222  reldisj  4404  ssundif  4438  ralidmw  4467  ralidm  4468  reuprg0  4658  raldifsni  4752  pwpw0  4768  unissb  4896  moabexOLD  5423  dffr2  5604  dffr2ALT  5605  dfepfr  5627  ssrel2  5753  dffr3  6084  opreu2reurex  6276  dffr4  6302  fncnv  6589  fun11  6590  dff13  7233  naddssim  8650  marypha2lem3  9377  dfsup2  9384  wemapsolem  9492  inf2  9572  axinf2  9589  aceq1  10067  aceq0  10068  kmlem14  10114  dfackm  10117  zfac  10411  ac6n  10436  zfcndrep  10566  zfcndac  10571  axgroth6  10780  axgroth4  10784  grothprim  10786  prime  12648  raluz2  12892  fsuppmapnn0ub  14002  mptnn0fsuppr  14006  brtrclfv  15009  rpnnen2lem12  16248  isprm2  16707  isprm4  16709  pgpfac1  20113  pgpfac  20117  isirred2  20457  isdomn5  20747  evl1maprhm  22430  pmatcollpw2lem  22825  isclo2  23136  lmres  23348  ist1-2  23395  is1stc2  23490  alexsubALTlem3  24097  itg2cn  25813  ellimc3  25929  plydivex  26349  vieta1  26364  dchrelbas2  27289  conway  27860  nmobndseqi  30939  nmobndseqiALT  30940  cvnbtwn3  32448  elat2  32500  inpr0  32691  ssrelf  32778  isarchi2  33326  archiabl  33339  islinds5  33514  1arithidom  33694  esumcvgre  34349  signstfvneq0  34827  hashreprin  34875  breprexp  34888  bnj1098  35040  bnj1533  35108  bnj121  35126  bnj124  35127  bnj130  35130  bnj153  35136  bnj207  35137  bnj611  35174  bnj864  35178  bnj865  35179  bnj1000  35197  bnj978  35205  bnj1021  35222  bnj1047  35229  bnj1049  35230  bnj1090  35235  bnj1110  35238  bnj1128  35246  bnj1145  35249  bnj1171  35256  bnj1172  35257  bnj1174  35259  bnj1176  35261  bnj1280  35276  axreg  35384  axregscl  35385  axinfprim  36017  dfon2lem9  36100  dffun10  36223  elicc3  36638  filnetlem4  36702  df3nandALT1  36720  df3nandALT2  36721  regsfromregtco  36859  regsfromunir1  36861  mh-infprim2bi  36868  bj-ssbeq  37086  bj-ax12ssb  37091  bj-alnnf  37173  qdiffALT  37781  pibt2  37872  poimirlem30  38110  inxpssidinxp  38782  cnvref5  38811  lcvnbtwn3  39613  isat3  39892  cdleme25cv  40943  cdlemefrs29bpre0  40981  cdlemk35  41497  dvrelogpow2b  42646  aks4d1p1p4  42649  aks6d1c2p2  42697  aks5lem3a  42767  aks5lem6  42770  unitscyglem2  42774  unitscyglem3  42775  sn-axrep5v  42797  supinf  42819  dford4  43567  ifpidg  44028  ifpid1g  44031  ifpim23g  44032  ifpororb  44042  ifpbibib  44047  elinintrab  44114  undmrnresiss  44141  cotrintab  44151  elintima  44190  frege60b  44442  frege91  44491  frege97  44497  frege98  44498  dffrege99  44499  frege109  44509  frege110  44510  frege131  44531  frege133  44533  ntrneiiso  44628  int-sqdefd  44718  int-sqgeq0d  44723  ismnuprim  44831  pm10.541  44904  pm13.196a  44951  2sbc6g  44952  expcomdg  45037  impexpd  45050  supxrleubrnmptf  45986  fsummulc1f  46108  fsumiunss  46112  fnlimfvre2  46212  limsupreuz  46272  lmbr3v  46280  dvmptmulf  46472  dvmptfprodlem  46479  sge0ltfirpmpt2  46961  hoidmv1le  47129  hoidmvle  47135  vonioolem2  47216  smflimlem3  47308  ldepslinc  49092  map0cor  49437  setrec1lem2  50270  setrec2  50277  sbidd-misc  50301