Theorem imbi2i 326

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

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

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 197

This theorem is referenced by:  iman  440  pm4.14  602  nan  604  pm5.32  668  anidmdbi  678  imimorb  921  pm5.6  951  nannan  1451  alimex  1758  19.36v  1904  19.36  2098  sblim  2397  sban  2399  sbhb  2438  2sb6  2444  mo2v  2477  moabs  2501  eu1  2510  r2allem  2937  r3al  2940  r19.21t  2955  r19.21v  2960  ralbii  2980  r19.35  3084  rspc2gv  3321  reu2  3394  reu8  3402  2reu5lem3  3415  ssconb  3743  ssin  3835  difin  3861  reldisj  4020  ssundif  4052  raldifsni  4324  pwpw0  4344  pwsnALT  4429  unissb  4469  moabex  4927  dffr2  5079  dfepfr  5099  ssrelOLD  5208  ssrel2  5210  dffr3  5498  dffr4  5696  fncnv  5962  fun11  5963  dff13  6512  marypha2lem3  8343  dfsup2  8350  wemapsolem  8455  inf2  8520  axinf2  8537  aceq1  8940  aceq0  8941  kmlem14  8985  dfackm  8988  zfac  9282  ac6n  9307  zfcndrep  9436  zfcndac  9441  axgroth6  9650  axgroth4  9654  grothprim  9656  prime  11458  raluz2  11737  fsuppmapnn0ub  12795  mptnn0fsuppr  12799  brtrclfv  13743  rpnnen2lem12  14954  isprm2  15395  isprm4  15397  pgpfac1  18479  pgpfac  18483  isirred2  18701  pmatcollpw2lem  20582  isclo2  20892  lmres  21104  ist1-2  21151  is1stc2  21245  alexsubALTlem3  21853  itg2cn  23530  ellimc3  23643  plydivex  24052  vieta1  24067  dchrelbas2  24962  nmobndseqi  27634  nmobndseqiALT  27635  cvnbtwn3  29147  elat2  29199  ssrelf  29425  funcnvmptOLD  29467  isarchi2  29739  archiabl  29752  esumcvgre  30153  signstfvneq0  30649  hashreprin  30698  breprexp  30711  bnj1098  30854  bnj1533  30922  bnj121  30940  bnj124  30941  bnj130  30944  bnj153  30950  bnj207  30951  bnj611  30988  bnj864  30992  bnj865  30993  bnj1000  31011  bnj978  31019  bnj1021  31034  bnj1047  31041  bnj1049  31042  bnj1090  31047  bnj1110  31050  bnj1128  31058  bnj1145  31061  bnj1171  31068  bnj1172  31069  bnj1174  31071  bnj1176  31073  bnj1280  31088  axinfprim  31583  dfon2lem9  31696  conway  31910  dffun10  32021  elicc3  32311  filnetlem4  32376  df3nandALT1  32396  df3nandALT2  32397  bj-ssbeq  32627  bj-ssb0  32628  bj-ax12ssb  32635  bj-ssbn  32641  bj-sbnf  32828  wl-nannan  33298  poimirlem30  33439  inxpssidinxp  34086  lcvnbtwn3  34315  isat3  34594  cdleme25cv  35646  cdlemefrs29bpre0  35684  cdlemk35  36200  dford4  37596  ifpidg  37836  ifpid1g  37839  ifpim23g  37840  ifpororb  37850  ifpbibib  37855  elinintrab  37883  undmrnresiss  37910  cotrintab  37921  elintima  37945  frege60b  38199  frege91  38248  frege97  38254  frege98  38255  dffrege99  38256  frege109  38266  frege110  38267  frege131  38288  frege133  38290  ntrneiiso  38389  int-sqdefd  38484  int-sqgeq0d  38489  pm10.541  38566  pm13.196a  38615  2sbc6g  38616  expcomdg  38706  impexpd  38719  jcn  39205  supxrleubrnmptf  39680  fsummulc1f  39802  fsumiunss  39807  fnlimfvre2  39909  limsupreuz  39969  limsupvaluz2  39970  lmbr3v  39977  dvmptmulf  40152  dvmptfprodlem  40159  sge0ltfirpmpt2  40643  hoidmv1le  40808  hoidmvle  40814  vonioolem2  40895  smflimlem3  40981  rmoanim  41179  ldepslinc  42298  setrec1lem2  42435  setrec2  42442  sbidd-misc  42460