Theorem imbi2i 336

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  iman  401  anidmdbi  565  pm5.32  573  pm4.14  806  nan  829  imimorb  952  pm5.6  1003  nannan  1498  alimex  1832  19.36v  1994  2sb6  2089  sbrimvw  2094  sbal  2172  19.36  2233  sbn  2282  sbrim  2306  sblim  2307  sbnfOLD  2314  cbvsbvf  2363  sbhb  2521  dfmo  2591  eu1  2605  r2allem  3120  r3al  3170  r19.21t  3226  rspc2gv  3582  reu2  3679  reu8  3687  2reu5lem3  3711  rmoanim  3840  rmoanimALT  3841  dfdif3OLD  4063  ssconb  4087  ssin  4184  difin  4217  reldisj  4398  ssundif  4433  ralidmw  4453  ralidm  4457  reuprg0  4650  raldifsni  4742  pwpw0  4760  unissb  4886  moabex  5394  dffr2  5572  dffr2ALT  5573  dfepfr  5595  ssrel2  5720  dffr3  6043  opreu2reurex  6236  dffr4  6262  fncnv  6549  fun11  6550  dff13  7183  naddssim  8595  marypha2lem3  9316  dfsup2  9323  wemapsolem  9431  inf2  9508  axinf2  9525  aceq1  10003  aceq0  10004  kmlem14  10050  dfackm  10053  zfac  10346  ac6n  10371  zfcndrep  10500  zfcndac  10505  axgroth6  10714  axgroth4  10718  grothprim  10720  prime  12549  raluz2  12790  fsuppmapnn0ub  13897  mptnn0fsuppr  13901  brtrclfv  14904  rpnnen2lem12  16129  isprm2  16588  isprm4  16590  pgpfac1  19989  pgpfac  19993  isirred2  20334  isdomn5  20620  evl1maprhm  22289  pmatcollpw2lem  22687  isclo2  22998  lmres  23210  ist1-2  23257  is1stc2  23352  alexsubALTlem3  23959  itg2cn  25686  ellimc3  25802  plydivex  26227  vieta1  26242  dchrelbas2  27170  conway  27735  nmobndseqi  30751  nmobndseqiALT  30752  cvnbtwn3  32260  elat2  32312  inpr0  32504  ssrelf  32590  isarchi2  33146  archiabl  33159  islinds5  33324  1arithidom  33494  esumcvgre  34096  signstfvneq0  34577  hashreprin  34625  breprexp  34638  bnj1098  34787  bnj1533  34856  bnj121  34874  bnj124  34875  bnj130  34878  bnj153  34884  bnj207  34885  bnj611  34922  bnj864  34926  bnj865  34927  bnj1000  34945  bnj978  34953  bnj1021  34970  bnj1047  34977  bnj1049  34978  bnj1090  34983  bnj1110  34986  bnj1128  34994  bnj1145  34997  bnj1171  35004  bnj1172  35005  bnj1174  35007  bnj1176  35009  bnj1280  35024  axreg  35117  axregscl  35118  axinfprim  35742  dfon2lem9  35825  dffun10  35948  elicc3  36351  filnetlem4  36415  df3nandALT1  36433  df3nandALT2  36434  bj-ssbeq  36687  bj-ax12ssb  36692  pibt2  37451  poimirlem30  37690  inxpssidinxp  38350  cnvref5  38379  lcvnbtwn3  39067  isat3  39346  cdleme25cv  40397  cdlemefrs29bpre0  40435  cdlemk35  40951  dvrelogpow2b  42101  aks4d1p1p4  42104  aks6d1c2p2  42152  aks5lem3a  42222  aks5lem6  42225  unitscyglem2  42229  unitscyglem3  42230  sn-axrep5v  42249  supinf  42275  dford4  43062  ifpidg  43524  ifpid1g  43527  ifpim23g  43528  ifpororb  43538  ifpbibib  43543  elinintrab  43610  undmrnresiss  43637  cotrintab  43647  elintima  43686  frege60b  43938  frege91  43987  frege97  43993  frege98  43994  dffrege99  43995  frege109  44005  frege110  44006  frege131  44027  frege133  44029  ntrneiiso  44124  int-sqdefd  44214  int-sqgeq0d  44219  ismnuprim  44327  pm10.541  44400  pm13.196a  44447  2sbc6g  44448  expcomdg  44533  impexpd  44546  supxrleubrnmptf  45489  fsummulc1f  45611  fsumiunss  45615  fnlimfvre2  45715  limsupreuz  45775  lmbr3v  45783  dvmptmulf  45975  dvmptfprodlem  45982  sge0ltfirpmpt2  46464  hoidmv1le  46632  hoidmvle  46638  vonioolem2  46719  smflimlem3  46811  ldepslinc  48541  map0cor  48886  setrec1lem2  49720  setrec2  49727  sbidd-misc  49751