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  2028  2sb6  2125  sbrimvwOLD  2131  sbal  2209  19.36  2270  sbn  2317  sbrim  2341  sblim  2342  cbvsbvf  2395  sbhb  2553  dfmo2  2624  eu1  2638  r2allem  3154  r3al  3204  r19.21t  3260  rspc2gv  3589  reu2  3686  reu8  3694  2reu5lem3  3718  rmoanim  3846  rmoanimALT  3847  ssconb  4081  ssin  4138  difin  4220  reldisj  4409  ssundif  4446  ralidmw  4475  ralidm  4476  reuprg0  4664  raldifsni  4760  pwpw0  4836  unissb  4906  moabexOLD  5434  dffr2  5619  dffr2ALT  5620  dfepfr  5642  ssrel2  5770  dffr3  6115  opreu2reurex  6323  dffr4  6349  fncnv  6643  fun11  6644  dff13  7289  naddssim  8733  marypha2lem3  9466  dfsup2  9473  wemapsolem  9581  inf2  9661  axinf2  9678  setrec1lem2  10004  setrec2  10014  aceq1  10235  aceq0  10236  kmlem14  10281  dfackm  10284  zfac  10577  ac6n  10602  zfcndrep  10738  zfcndac  10743  axgroth6  10952  axgroth4  10956  grothprim  10958  prime  12820  raluz2  13064  fsuppmapnn0ub  14178  mptnn0fsuppr  14182  brtrclfv  15198  rpnnen2lem12  16437  isprm2  16901  isprm4  16903  pgpfac1  20347  pgpfac  20351  isirred2  20702  isdomn5  21013  evl1maprhm  22752  pmatcollpw2lem  23150  isclo2  23461  lmres  23673  ist1-2  23720  is1stc2  23815  alexsubALTlem3  24423  itg2cn  26139  ellimc3  26254  plydivex  26673  vieta1  26690  dchrelbas2  27621  conway  28222  nmobndseqi  31438  nmobndseqiALT  31439  cvnbtwn3  32947  elat2  32999  inpr0  33226  ssrelf  33307  isarchi2  33845  archiabl  33858  islinds5  34027  1arithidom  34173  esumcvgre  34834  signstfvneq0  35312  hashreprin  35360  breprexp  35373  bnj1098  35525  bnj1533  35593  bnj121  35611  bnj124  35612  bnj130  35615  bnj153  35621  bnj207  35622  bnj611  35659  bnj864  35663  bnj865  35664  bnj1000  35682  bnj978  35690  bnj1021  35707  bnj1047  35714  bnj1049  35715  bnj1090  35720  bnj1110  35723  bnj1128  35731  bnj1145  35734  bnj1171  35741  bnj1172  35742  bnj1174  35744  bnj1176  35746  bnj1280  35761  axreg  35936  axregscl  35937  axinfprim  36686  dfon2lem9  36768  dffun10  36891  elicc3  37320  filnetlem4  37384  df3nandALT1  37402  df3nandALT2  37403  regsfromregtco  37541  regsfromunir1  37543  mh-infprim2bi  37550  bj-ssbeq  37767  bj-ax12ssb  37772  bj-alnnf  37854  bj-cossid  38209  cocnv1ssid  38211  cocnv2ssid  38214  qdiffALT  38517  pibt2  38608  poimirlem30  38836  inxpssidinxp  39520  cnvref5  39549  lcvnbtwn3  40351  isat3  40630  cdleme25cv  41681  cdlemefrs29bpre0  41719  cdlemk35  42235  dvrelogpow2b  43384  aks4d1p1p4  43387  aks6d1c2p2  43435  aks5lem3a  43505  aks5lem6  43508  unitscyglem2  43512  unitscyglem3  43513  sn-axrep5v  43538  supinf  43560  dford4  44302  ifpidg  44753  ifpid1g  44756  ifpim23g  44757  ifpororb  44767  ifpbibib  44772  elinintrab  44839  undmrnresiss  44865  cotrintab  44875  elintima  44914  frege60b  45166  frege91  45215  frege97  45221  frege98  45222  dffrege99  45223  frege109  45233  frege110  45234  frege131  45255  frege133  45257  ntrneiiso  45352  int-sqdefd  45442  int-sqgeq0d  45447  ismnuprim  45539  pm10.541  45612  pm13.196a  45659  2sbc6g  45660  expcomdg  45743  impexpd  45756  supxrleubrnmptf  46734  fsummulc1f  46856  fsumiunss  46860  fnlimfvre2  46960  limsupreuz  47020  lmbr3v  47028  dvmptmulf  47220  dvmptfprodlem  47227  sge0ltfirpmpt2  47709  hoidmv1le  47877  hoidmvle  47883  vonioolem2  47964  smflimlem3  48056  ldepslinc  49952  map0cor  50297  sbidd-misc  51218