Theorem imbi2i 310

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  422  pm4.14  576  nan  578  pm5.32  634  anidmdbi  644  imimorb  878  pm5.6  913  nannan  1350  alimex  1673  19.36v  1786  19.36  1992  sblim  2162  sban  2164  sbhb  2206  2sb6  2212  mo2v  2245  mo2vOLD  2246  mo2vOLDOLD  2247  moabs  2271  eu1  2282  2eu6OLD  2335  r2allem  2779  r2alfOLD  2781  r3al  2784  r19.21t  2801  r19.21tOLD  2802  r19.21v  2809  ralbii  2835  r19.35  2954  reu2  3237  reu8  3245  2reu5lem3  3257  ssconb  3576  ssin  3661  difin  3687  reldisj  3813  ssundif  3855  raldifsni  4102  pwpw0  4120  pwsnALT  4186  unissb  4222  moabex  4650  dffr2  4788  dfepfr  4808  ssrel  4912  ssrel2  4914  dffr3  5189  dffr4  5383  fncnv  5633  fun11  5634  dff13  6147  marypha2lem3  7931  dfsup2  7936  wemapsolem  8009  inf2  8073  axinf2  8090  aceq1  8530  aceq0  8531  kmlem14  8575  dfackm  8578  zfac  8872  ac6n  8897  zfcndrep  9022  zfcndac  9027  axgroth6  9236  axgroth4  9240  grothprim  9242  prime  10984  raluz2  11176  fsuppmapnn0ub  12145  mptnn0fsuppr  12149  brtrclfv  12985  rpnnen2  14168  isprm2  14434  isprm4  14436  pgpfac1  17451  pgpfac  17455  isirred2  17670  pmatcollpw2lem  19570  isclo2  19882  lmres  20094  ist1-2  20141  is1stc2  20235  alexsubALTlem3  20841  itg2cn  22462  ellimc3  22575  plydivex  22985  vieta1  23000  dchrelbas2  23893  nmobndseqi  26108  nmobndseqiALT  26109  cvnbtwn3  27620  elat2  27672  ssrelf  27903  funcnvmptOLD  27952  isarchi2  28181  archiabl  28194  esumcvgre  28538  signstfvneq0  29035  bnj1098  29169  bnj1533  29237  bnj121  29255  bnj124  29256  bnj130  29259  bnj153  29265  bnj207  29266  bnj611  29303  bnj864  29307  bnj865  29308  bnj1000  29326  bnj978  29334  bnj1021  29349  bnj1047  29356  bnj1049  29357  bnj1090  29362  bnj1110  29365  bnj1128  29373  bnj1145  29376  bnj1171  29383  bnj1172  29384  bnj1174  29386  bnj1176  29388  bnj1280  29403  axinfprim  29907  dfon2lem9  30010  dffun10  30252  elicc3  30545  filnetlem4  30609  df3nandALT1  30629  df3nandALT2  30630  bj-sbnf  30976  wl-nannan  31340  lcvnbtwn3  32046  isat3  32325  cdleme25cv  33377  cdlemefrs29bpre0  33415  cdlemk35  33931  dford4  35333  ifpidg  35582  ifpid1g  35585  ifpim23g  35586  ifpororb  35596  ifpbibib  35601  elintima  35632  frege60b  35886  frege91  35935  frege97  35941  frege98  35942  dffrege99  35943  frege109  35953  frege110  35954  frege131  35975  frege133  35977  int-rightdistd  36012  int-sqdefd  36013  int-sqgeq0d  36018  pm10.541  36120  pm13.196a  36169  2sbc6g  36170  expcomdg  36286  impexpd  36300  jcn  36803  fsummulc1f  36937  dvmptmulf  37102  dvmptfprodlem  37109  rmoanim  37552  ldepslinc  38621  sbidd-misc  38759