Theorem imbi2i 314

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	|- ( ph <-> ps )

Assertion

Ref	Expression
imbi2i	|- ( ( ch -> ph ) <-> ( ch -> ps ) )

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		imbi2i.1	. . 3 |- ( ph <-> ps )
2	1	a1i 11	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.74i 249	1 |- ( ( ch -> ph ) <-> ( ch -> ps ) )

Syntax hints:   -> wi 4   <-> wb 188

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 189

This theorem is referenced by:  iman  426  pm4.14  581  nan  583  pm5.32  641  anidmdbi  651  imimorb  886  pm5.6  921  nannan  1385  alimex  1700  19.36v  1810  19.36  2020  sblim  2192  sban  2194  sbhb  2234  2sb6  2240  mo2v  2273  mo2vOLD  2274  moabs  2298  eu1  2307  r2allem  2801  r2alfOLD  2803  r3al  2806  r19.21t  2823  r19.21tOLD  2824  r19.21v  2831  ralbii  2857  r19.35  2976  reu2  3260  reu8  3268  2reu5lem3  3280  ssconb  3599  ssin  3685  difin  3711  reldisj  3837  ssundif  3880  raldifsni  4128  pwpw0  4146  pwsnALT  4212  unissb  4248  moabex  4678  dffr2  4816  dfepfr  4836  ssrel  4940  ssrel2  4942  dffr3  5218  dffr4  5413  fncnv  5663  fun11  5664  dff13  6172  marypha2lem3  7955  dfsup2  7962  wemapsolem  8069  inf2  8132  axinf2  8149  aceq1  8550  aceq0  8551  kmlem14  8595  dfackm  8598  zfac  8892  ac6n  8917  zfcndrep  9041  zfcndac  9046  axgroth6  9255  axgroth4  9259  grothprim  9261  prime  11018  raluz2  11210  fsuppmapnn0ub  12208  mptnn0fsuppr  12212  brtrclfv  13060  rpnnen2  14271  isprm2  14625  isprm4  14627  pgpfac1  17706  pgpfac  17710  isirred2  17922  pmatcollpw2lem  19793  isclo2  20096  lmres  20308  ist1-2  20355  is1stc2  20449  alexsubALTlem3  21056  itg2cn  22713  ellimc3  22826  plydivex  23242  vieta1  23257  dchrelbas2  24157  nmobndseqi  26412  nmobndseqiALT  26413  cvnbtwn3  27933  elat2  27985  ssrelf  28217  funcnvmptOLD  28266  isarchi2  28503  archiabl  28516  esumcvgre  28914  signstfvneq0  29463  bnj1098  29597  bnj1533  29665  bnj121  29683  bnj124  29684  bnj130  29687  bnj153  29693  bnj207  29694  bnj611  29731  bnj864  29735  bnj865  29736  bnj1000  29754  bnj978  29762  bnj1021  29777  bnj1047  29784  bnj1049  29785  bnj1090  29790  bnj1110  29793  bnj1128  29801  bnj1145  29804  bnj1171  29811  bnj1172  29812  bnj1174  29814  bnj1176  29816  bnj1280  29831  axinfprim  30335  dfon2lem9  30438  dffun10  30680  elicc3  30972  filnetlem4  31036  df3nandALT1  31056  df3nandALT2  31057  bj-sbnf  31405  wl-nannan  31811  poimirlem30  31928  lcvnbtwn3  32557  isat3  32836  cdleme25cv  33888  cdlemefrs29bpre0  33926  cdlemk35  34442  dford4  35848  ifpidg  36099  ifpid1g  36102  ifpim23g  36103  ifpororb  36113  ifpbibib  36118  elintima  36149  frege60b  36403  frege91  36452  frege97  36458  frege98  36459  dffrege99  36460  frege109  36470  frege110  36471  frege131  36492  frege133  36494  int-rightdistd  36529  int-sqdefd  36530  int-sqgeq0d  36535  pm10.541  36618  pm13.196a  36667  2sbc6g  36668  expcomdg  36758  impexpd  36772  jcn  37273  fsummulc1f  37514  fsumiunss  37521  dvmptmulf  37676  dvmptfprodlem  37683  sge0ltfirpmpt2  38100  rmoanim  38357  ldepslinc  39646  sbidd-misc  39783