Theorem imbi2i 312

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

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

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 185

This theorem is referenced by:  iman  424  pm4.14  578  nan  580  pm5.32  636  anidmdbi  646  imimorb  877  pm5.6  912  nannan  1348  alimex  1653  19.36v  1763  19.36  1965  sblim  2139  sban  2141  sbhb  2183  2sb6  2189  mo2v  2290  mo2vOLD  2291  mo2vOLDOLD  2292  moabs  2316  eu1  2328  2eu6OLD  2384  r2allem  2832  r2alfOLD  2834  r3al  2837  r19.21t  2854  r19.21tOLD  2855  r19.21v  2862  ralbii  2888  r19.35  3004  reu2  3287  reu8  3295  2reu5lem3  3307  ssconb  3633  ssin  3716  difin  3742  reldisj  3873  ssundif  3914  raldifsni  4162  pwpw0  4180  pwsnALT  4246  unissb  4283  moabex  4715  dffr2  4853  dfepfr  4873  ssrel  5100  ssrel2  5102  dffr3  5379  fncnv  5658  fun11  5659  dff13  6167  marypha2lem3  7915  dfsup2  7920  wemapsolem  7993  inf2  8057  axinf2  8074  aceq1  8515  aceq0  8516  kmlem14  8560  dfackm  8563  zfac  8857  ac6n  8882  zfcndrep  9009  zfcndac  9014  axgroth6  9223  axgroth4  9227  grothprim  9229  prime  10964  raluz2  11155  fsuppmapnn0ub  12103  mptnn0fsuppr  12107  rpnnen2  13970  isprm2  14236  isprm4  14238  pgpfac1  17257  pgpfac  17261  isirred2  17476  pmatcollpw2lem  19404  isclo2  19715  lmres  19927  ist1-2  19974  is1stc2  20068  alexsubALTlem3  20674  itg2cn  22295  ellimc3  22408  plydivex  22818  vieta1  22833  dchrelbas2  23637  nmobndseqi  25820  nmobndseqiALT  25821  cvnbtwn3  27333  elat2  27385  ssrelf  27604  funcnvmptOLD  27657  isarchi2  27881  archiabl  27894  esumcvgre  28251  signstfvneq0  28704  axinfprim  29253  dfon2lem9  29397  dffr4  29436  dffun10  29726  df3nandALT1  30024  df3nandALT2  30025  elicc3  30297  filnetlem4  30361  dford4  31133  pm10.541  31434  pm13.196a  31483  2sbc6g  31484  jcn  31588  fsummulc1f  31730  dvmptmulf  31895  dvmptfprodlem  31902  rmoanim  32345  ldepslinc  33212  sbidd-misc  33215  expcomdg  33370  impexpd  33384  bnj1098  33943  bnj1533  34011  bnj121  34029  bnj124  34030  bnj130  34033  bnj153  34039  bnj207  34040  bnj611  34077  bnj864  34081  bnj865  34082  bnj1000  34100  bnj978  34108  bnj1021  34123  bnj1047  34130  bnj1049  34131  bnj1090  34136  bnj1110  34139  bnj1128  34147  bnj1145  34150  bnj1171  34157  bnj1172  34158  bnj1174  34160  bnj1176  34162  bnj1280  34177  bj-sbnf  34513  lcvnbtwn3  34854  isat3  35133  cdleme25cv  36185  cdlemefrs29bpre0  36223  cdlemk35  36739  bj-ifidg  37808  bj-ifid1g  37809  bj-ifbibib  37822  bj-ifororb  37827  elintima  37866  frege60b  38033  int-rightdistd  38102  int-sqdefd  38103  int-sqgeq0d  38108