Theorem imbi1i 316

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

Ref	Expression
imbi1i.1	|- ( ph <-> ps )

Assertion

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

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 |- ( ph <-> ps )
2		imbi1 314	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ch ) <-> ( ps -> ch ) ) )
3	1, 2	ax-mp 8	1 |- ( ( ph -> ch ) <-> ( ps -> ch ) )

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

This theorem is referenced by:  imbi12i  317  imor  402  ancomsimp  1375  19.43  1612  19.37  1890  dfsb3  2105  sbor  2115  sbrim  2116  mo4f  2286  2mos  2333  neor  2651  r3al  2723  r19.23t  2780  r19.43  2823  ceqsralt  2939  ralab  3055  ralrab  3056  euind  3081  reu2  3082  rmo4  3087  reuind  3097  2reu5lem3  3101  rmo3  3208  raldifb  3447  unss  3481  ralunb  3488  inssdif0  3655  ssundif  3671  dfif2  3701  pwss  3773  ralsns  3804  disjsn  3828  snss  3886  unissb  4005  intun  4042  intpr  4043  dfiin2g  4084  disjor  4156  dftr2  4264  axrep1  4281  axpweq  4336  zfpow  4338  axpow2  4339  zfun  4661  uniex2  4663  reusv2lem4  4686  reusv2  4688  reusv7OLD  4694  dfom2  4806  raliunxp  4973  asymref2  5210  dffun2  5423  dffun4  5425  dffun5  5426  dffun7  5438  fununi  5476  dff13  5963  fimaxg  7313  fiint  7342  dfsup2  7405  oemapso  7594  scottexs  7767  scott0s  7768  iscard2  7819  acnnum  7889  dfac9  7972  dfacacn  7977  kmlem4  7989  kmlem12  7997  axpowndlem3  8430  zfcndun  8446  zfcndpow  8447  zfcndac  8450  axgroth5  8655  grothpw  8657  axgroth6  8659  infm3  9923  raluz2  10482  nnwos  10500  ralrp  10586  lo1resb  12313  rlimresb  12314  o1resb  12315  isprm4  13044  acsfn1  13841  acsfn2  13843  lubid  14394  isirred2  15761  isdomn2  16314  iunocv  16863  ist1-2  17365  isnrm2  17376  dfcon2  17435  alexsubALTlem3  18033  ismbl  19375  dyadmbllem  19444  ellimc3  19719  dchrelbas2  20974  dchrelbas3  20975  isch2  22679  choc0  22781  h1dei  23005  mdsl2i  23778  xfree2  23901  rmo3f  23935  rmo4fOLD  23936  rmo4f  23937  disjorf  23974  axextprim  25103  axunprim  25105  axpowprim  25106  untuni  25111  3orit  25122  biimpexp  25126  dfon2lem8  25360  predreseq  25393  soseq  25468  dfom5b  25666  raldifsni  26624  fphpd  26767  dford4  26990  fnwe2lem2  27016  islindf4  27176  isdomn3  27391  pm14.12  27489  raldifsnb  27946  dff14b  27960  dfvd2an  28383  dfvd3  28392  dfvd3an  28395  uun2221  28634  uun2221p1  28635  uun2221p2  28636  bnj538  28814  bnj1101  28861  bnj1109  28863  bnj1533  28929  bnj580  28990  bnj864  28999  bnj865  29000  bnj978  29026  bnj1049  29049  bnj1090  29054  bnj1145  29068  sborNEW7  29270  sbrimNEW7  29271  dfsb3NEW7  29340  cvlsupr3  29827  pmapglbx  30251  isltrn2N  30602  cdlemefrs29bpre0  30878

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178