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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  jcndOLD  340  iman  405  anidmdbi  569  pm5.32  577  pm4.14  807  nan  830  imimorb  951  pm5.6  1002  nannan  1493  alimex  1838  19.36v  1996  2sb6  2092  sbrimvlem  2097  sbal  2163  19.36  2228  sbn  2281  sblim  2307  sbievg  2362  sbhb  2524  dfmo  2595  eu1  2611  r19.21v  3098  r2allem  3121  r3al  3123  r19.21t  3135  nfra2w  3149  rspc2gv  3546  reu2  3638  reu8  3646  2reu5lem3  3670  rmoanim  3806  rmoanimALT  3807  dfdif3  4029  ssconb  4052  ssin  4145  difin  4176  reldisj  4366  reldisjOLD  4367  ssundif  4399  ralidmw  4419  ralidm  4423  reuprg0  4618  raldifsni  4708  pwpw0  4726  pwsnOLD  4812  unissb  4853  moabex  5343  dffr2  5515  dffr2ALT  5516  dfepfr  5536  ssrel2  5656  dffr3  5967  opreu2reurex  6157  dffr4  6178  fncnv  6453  fun11  6454  dff13  7067  marypha2lem3  9053  dfsup2  9060  wemapsolem  9166  inf2  9238  axinf2  9255  aceq1  9731  aceq0  9732  kmlem14  9777  dfackm  9780  zfac  10074  ac6n  10099  zfcndrep  10228  zfcndac  10233  axgroth6  10442  axgroth4  10446  grothprim  10448  prime  12258  raluz2  12493  fsuppmapnn0ub  13568  mptnn0fsuppr  13572  brtrclfv  14565  rpnnen2lem12  15786  isprm2  16239  isprm4  16241  pgpfac1  19467  pgpfac  19471  isirred2  19719  pmatcollpw2lem  21674  isclo2  21985  lmres  22197  ist1-2  22244  is1stc2  22339  alexsubALTlem3  22946  itg2cn  24661  ellimc3  24776  plydivex  25190  vieta1  25205  dchrelbas2  26118  nmobndseqi  28860  nmobndseqiALT  28861  cvnbtwn3  30369  elat2  30421  inpr0  30599  ssrelf  30674  isarchi2  31158  archiabl  31171  islinds5  31277  esumcvgre  31771  signstfvneq0  32263  hashreprin  32312  breprexp  32325  bnj1098  32476  bnj1533  32545  bnj121  32563  bnj124  32564  bnj130  32567  bnj153  32573  bnj207  32574  bnj611  32611  bnj864  32615  bnj865  32616  bnj1000  32634  bnj978  32642  bnj1021  32659  bnj1047  32666  bnj1049  32667  bnj1090  32672  bnj1110  32675  bnj1128  32683  bnj1145  32686  bnj1171  32693  bnj1172  32694  bnj1174  32696  bnj1176  32698  bnj1280  32713  axinfprim  33360  dfon2lem9  33486  naddssim  33574  conway  33730  dffun10  33953  elicc3  34243  filnetlem4  34307  df3nandALT1  34325  df3nandALT2  34326  bj-ssbeq  34571  bj-ax12ssb  34576  bj-sbnf  34761  pibt2  35325  poimirlem30  35544  inxpssidinxp  36188  lcvnbtwn3  36779  isat3  37058  cdleme25cv  38109  cdlemefrs29bpre0  38147  cdlemk35  38663  dvrelogpow2b  39809  aks4d1p1p4  39812  metakunt6  39852  metakunt24  39870  2xp3dxp2ge1d  39884  isdomn5  39893  sn-axrep5v  39907  dford4  40554  ifpidg  40783  ifpid1g  40786  ifpim23g  40787  ifpororb  40797  ifpbibib  40802  elinintrab  40861  undmrnresiss  40888  cotrintab  40898  elintima  40938  frege60b  41190  frege91  41239  frege97  41245  frege98  41246  dffrege99  41247  frege109  41257  frege110  41258  frege131  41279  frege133  41281  ntrneiiso  41378  int-sqdefd  41470  int-sqgeq0d  41475  ismnuprim  41585  pm10.541  41658  pm13.196a  41705  2sbc6g  41706  expcomdg  41793  impexpd  41806  supxrleubrnmptf  42666  fsummulc1f  42787  fsumiunss  42791  fnlimfvre2  42893  limsupreuz  42953  limsupvaluz2  42954  lmbr3v  42961  dvmptmulf  43153  dvmptfprodlem  43160  sge0ltfirpmpt2  43639  hoidmv1le  43807  hoidmvle  43813  vonioolem2  43894  smflimlem3  43980  ldepslinc  45523  map0cor  45855  setrec1lem2  46065  setrec2  46072  sbidd-misc  46092