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  2207  19.36  2269  sbn  2317  sbrim  2341  sblim  2342  cbvsbvf  2397  sbhb  2555  dfmo2  2626  eu1  2640  r2allem  3155  r3al  3205  r19.21t  3261  rspc2gv  3593  reu2  3690  reu8  3698  2reu5lem3  3722  rmoanim  3849  rmoanimALT  3850  ssconb  4096  ssin  4191  difin  4225  reldisj  4413  ssundif  4450  ralidmw  4479  ralidm  4480  reuprg0  4670  raldifsni  4765  pwpw0  4781  unissb  4908  moabexOLD  5442  dffr2  5624  dffr2ALT  5625  dfepfr  5647  ssrel2  5773  dffr3  6103  opreu2reurex  6299  dffr4  6325  fncnv  6613  fun11  6614  dff13  7257  naddssim  8678  marypha2lem3  9404  dfsup2  9411  wemapsolem  9519  inf2  9599  axinf2  9616  aceq1  10117  aceq0  10118  kmlem14  10163  dfackm  10166  zfac  10459  ac6n  10484  zfcndrep  10614  zfcndac  10619  axgroth6  10828  axgroth4  10832  grothprim  10834  prime  12693  raluz2  12937  fsuppmapnn0ub  14049  mptnn0fsuppr  14053  brtrclfv  15063  rpnnen2lem12  16303  isprm2  16762  isprm4  16764  pgpfac1  20196  pgpfac  20200  isirred2  20549  isdomn5  20859  evl1maprhm  22589  pmatcollpw2lem  22984  isclo2  23295  lmres  23507  ist1-2  23554  is1stc2  23649  alexsubALTlem3  24257  itg2cn  25973  ellimc3  26089  plydivex  26509  vieta1  26524  dchrelbas2  27452  conway  28023  nmobndseqi  31202  nmobndseqiALT  31203  cvnbtwn3  32711  elat2  32763  inpr0  32949  ssrelf  33031  isarchi2  33569  archiabl  33582  islinds5  33746  1arithidom  33891  esumcvgre  34545  signstfvneq0  35024  hashreprin  35072  breprexp  35085  bnj1098  35237  bnj1533  35305  bnj121  35323  bnj124  35324  bnj130  35327  bnj153  35333  bnj207  35334  bnj611  35371  bnj864  35375  bnj865  35376  bnj1000  35394  bnj978  35402  bnj1021  35419  bnj1047  35426  bnj1049  35427  bnj1090  35432  bnj1110  35435  bnj1128  35443  bnj1145  35446  bnj1171  35453  bnj1172  35454  bnj1174  35456  bnj1176  35458  bnj1280  35473  axreg  35597  axregscl  35598  axinfprim  36235  dfon2lem9  36318  dffun10  36441  elicc3  36885  filnetlem4  36949  df3nandALT1  36967  df3nandALT2  36968  regsfromregtco  37106  regsfromunir1  37108  mh-infprim2bi  37115  bj-ssbeq  37332  bj-ax12ssb  37337  bj-alnnf  37419  qdiffALT  38029  pibt2  38120  poimirlem30  38358  inxpssidinxp  39029  cnvref5  39058  lcvnbtwn3  39860  isat3  40139  cdleme25cv  41190  cdlemefrs29bpre0  41228  cdlemk35  41744  dvrelogpow2b  42893  aks4d1p1p4  42896  aks6d1c2p2  42944  aks5lem3a  43014  aks5lem6  43017  unitscyglem2  43021  unitscyglem3  43022  sn-axrep5v  43046  supinf  43068  dford4  43814  ifpidg  44275  ifpid1g  44278  ifpim23g  44279  ifpororb  44289  ifpbibib  44294  elinintrab  44361  undmrnresiss  44388  cotrintab  44398  elintima  44437  frege60b  44689  frege91  44738  frege97  44744  frege98  44745  dffrege99  44746  frege109  44756  frege110  44757  frege131  44778  frege133  44780  ntrneiiso  44875  int-sqdefd  44965  int-sqgeq0d  44970  ismnuprim  45062  pm10.541  45135  pm13.196a  45182  2sbc6g  45183  expcomdg  45267  impexpd  45280  supxrleubrnmptf  46223  fsummulc1f  46345  fsumiunss  46349  fnlimfvre2  46449  limsupreuz  46509  lmbr3v  46517  dvmptmulf  46709  dvmptfprodlem  46716  sge0ltfirpmpt2  47198  hoidmv1le  47366  hoidmvle  47372  vonioolem2  47453  smflimlem3  47545  ldepslinc  49346  map0cor  49690  setrec1lem2  50523  setrec2  50530  sbidd-misc  50554