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  582  nan  584  pm5.32  642  anidmdbi  652  imimorb  888  pm5.6  923  nannan  1389  alimex  1703  19.36v  1820  19.36  2044  sblim  2226  sban  2228  sbhb  2267  2sb6  2273  mo2v  2306  moabs  2330  eu1  2339  r2allem  2763  r2alfOLD  2765  r3al  2768  r19.21t  2785  r19.21tOLD  2786  r19.21v  2793  ralbii  2819  r19.35  2937  reu2  3226  reu8  3234  2reu5lem3  3247  ssconb  3566  ssin  3654  difin  3680  reldisj  3808  ssundif  3851  raldifsni  4102  pwpw0  4120  pwsnALT  4193  unissb  4229  moabex  4659  dffr2  4799  dfepfr  4819  ssrel  4923  ssrel2  4925  dffr3  5201  dffr4  5396  fncnv  5647  fun11  5648  dff13  6159  marypha2lem3  7951  dfsup2  7958  wemapsolem  8065  inf2  8128  axinf2  8145  aceq1  8548  aceq0  8549  kmlem14  8593  dfackm  8596  zfac  8890  ac6n  8915  zfcndrep  9039  zfcndac  9044  axgroth6  9253  axgroth4  9257  grothprim  9259  prime  11016  raluz2  11208  fsuppmapnn0ub  12207  mptnn0fsuppr  12211  brtrclfv  13066  rpnnen2  14278  isprm2  14632  isprm4  14634  pgpfac1  17713  pgpfac  17717  isirred2  17929  pmatcollpw2lem  19801  isclo2  20104  lmres  20316  ist1-2  20363  is1stc2  20457  alexsubALTlem3  21064  itg2cn  22721  ellimc3  22834  plydivex  23250  vieta1  23265  dchrelbas2  24165  nmobndseqi  26420  nmobndseqiALT  26421  cvnbtwn3  27941  elat2  27993  ssrelf  28221  funcnvmptOLD  28270  isarchi2  28502  archiabl  28515  esumcvgre  28912  signstfvneq0  29461  bnj1098  29595  bnj1533  29663  bnj121  29681  bnj124  29682  bnj130  29685  bnj153  29691  bnj207  29692  bnj611  29729  bnj864  29733  bnj865  29734  bnj1000  29752  bnj978  29760  bnj1021  29775  bnj1047  29782  bnj1049  29783  bnj1090  29788  bnj1110  29791  bnj1128  29799  bnj1145  29802  bnj1171  29809  bnj1172  29810  bnj1174  29812  bnj1176  29814  bnj1280  29829  axinfprim  30333  dfon2lem9  30437  dffun10  30681  elicc3  30973  filnetlem4  31037  df3nandALT1  31057  df3nandALT2  31058  bj-ssbeq  31240  bj-ssb0  31241  bj-ax12ssb  31248  bj-ssbn  31254  bj-sbnf  31441  wl-nannan  31853  poimirlem30  31970  lcvnbtwn3  32594  isat3  32873  cdleme25cv  33925  cdlemefrs29bpre0  33963  cdlemk35  34479  dford4  35884  ifpidg  36135  ifpid1g  36138  ifpim23g  36139  ifpororb  36149  ifpbibib  36154  elinintrab  36183  undmrnresiss  36210  cotrintab  36221  elintima  36245  frege60b  36501  frege91  36550  frege97  36556  frege98  36557  dffrege99  36558  frege109  36568  frege110  36569  frege131  36590  frege133  36592  int-rightdistd  36627  int-sqdefd  36628  int-sqgeq0d  36633  pm10.541  36716  pm13.196a  36765  2sbc6g  36766  expcomdg  36856  impexpd  36870  jcn  37368  fsummulc1f  37647  fsumiunss  37654  dvmptmulf  37812  dvmptfprodlem  37819  sge0ltfirpmpt2  38268  hoidmv1le  38416  hoidmvle  38422  rmoanim  38600  ldepslinc  40355  sbidd-misc  40492