Theorem imbi2i 339

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  iman  407  anidmdbi  576  pm5.32  584  pm4.14  819  nan  843  imimorb  965  pm5.6  1017  nannan  1527  alimex  1864  19.36v  2026  2sb6  2123  sbrimvwOLD  2129  sbal  2206  19.36  2267  sbn  2314  sbrim  2338  sblim  2339  cbvsbvf  2393  sbhb  2551  dfmo2  2622  eu1  2636  r2allem  3151  r3al  3201  r19.21t  3257  rspc2gv  3586  reu2  3683  reu8  3691  2reu5lem3  3715  rmoanim  3842  rmoanimALT  3843  ssconb  4089  ssin  4184  difin  4218  reldisj  4406  ssundif  4443  ralidmw  4472  ralidm  4473  reuprg0  4663  raldifsni  4758  pwpw0  4774  unissb  4901  moabexOLD  5427  dffr2  5612  dffr2ALT  5613  dfepfr  5635  ssrel2  5761  dffr3  6097  opreu2reurex  6296  dffr4  6322  fncnv  6611  fun11  6612  dff13  7256  naddssim  8688  marypha2lem3  9422  dfsup2  9429  wemapsolem  9537  inf2  9617  axinf2  9634  setrec1lem2  9960  setrec2  9970  aceq1  10189  aceq0  10190  kmlem14  10235  dfackm  10238  zfac  10531  ac6n  10556  zfcndrep  10692  zfcndac  10697  axgroth6  10906  axgroth4  10910  grothprim  10912  prime  12773  raluz2  13017  fsuppmapnn0ub  14131  mptnn0fsuppr  14135  brtrclfv  15148  rpnnen2lem12  16386  isprm2  16850  isprm4  16852  pgpfac1  20289  pgpfac  20293  isirred2  20644  isdomn5  20955  evl1maprhm  22690  pmatcollpw2lem  23088  isclo2  23399  lmres  23611  ist1-2  23658  is1stc2  23753  alexsubALTlem3  24361  itg2cn  26077  ellimc3  26192  plydivex  26611  vieta1  26628  dchrelbas2  27557  conway  28158  nmobndseqi  31374  nmobndseqiALT  31375  cvnbtwn3  32883  elat2  32935  inpr0  33121  ssrelf  33202  isarchi2  33739  archiabl  33752  islinds5  33916  1arithidom  34062  esumcvgre  34716  signstfvneq0  35194  hashreprin  35242  breprexp  35255  bnj1098  35407  bnj1533  35475  bnj121  35493  bnj124  35494  bnj130  35497  bnj153  35503  bnj207  35504  bnj611  35541  bnj864  35545  bnj865  35546  bnj1000  35564  bnj978  35572  bnj1021  35589  bnj1047  35596  bnj1049  35597  bnj1090  35602  bnj1110  35605  bnj1128  35613  bnj1145  35616  bnj1171  35623  bnj1172  35624  bnj1174  35626  bnj1176  35628  bnj1280  35643  axreg  35778  axregscl  35779  axinfprim  36450  dfon2lem9  36533  dffun10  36656  elicc3  37085  filnetlem4  37149  df3nandALT1  37167  df3nandALT2  37168  regsfromregtco  37306  regsfromunir1  37308  mh-infprim2bi  37315  bj-ssbeq  37532  bj-ax12ssb  37537  bj-alnnf  37619  qdiffALT  38229  pibt2  38320  poimirlem30  38548  inxpssidinxp  39234  cnvref5  39263  lcvnbtwn3  40065  isat3  40344  cdleme25cv  41395  cdlemefrs29bpre0  41433  cdlemk35  41949  dvrelogpow2b  43098  aks4d1p1p4  43101  aks6d1c2p2  43149  aks5lem3a  43219  aks5lem6  43222  unitscyglem2  43226  unitscyglem3  43227  sn-axrep5v  43251  supinf  43273  dford4  44015  ifpidg  44476  ifpid1g  44479  ifpim23g  44480  ifpororb  44490  ifpbibib  44495  elinintrab  44562  undmrnresiss  44589  cotrintab  44599  elintima  44638  frege60b  44890  frege91  44939  frege97  44945  frege98  44946  dffrege99  44947  frege109  44957  frege110  44958  frege131  44979  frege133  44981  ntrneiiso  45076  int-sqdefd  45166  int-sqgeq0d  45171  ismnuprim  45263  pm10.541  45336  pm13.196a  45383  2sbc6g  45384  expcomdg  45468  impexpd  45481  supxrleubrnmptf  46430  fsummulc1f  46552  fsumiunss  46556  fnlimfvre2  46656  limsupreuz  46716  lmbr3v  46724  dvmptmulf  46916  dvmptfprodlem  46923  sge0ltfirpmpt2  47405  hoidmv1le  47573  hoidmvle  47579  vonioolem2  47660  smflimlem3  47752  ldepslinc  49590  map0cor  49934  sbidd-misc  50781