Theorem imbi1i 325

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 323	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ch ) <-> ( ps -> ch ) ) )
3	1, 2	ax-mp 5	1 |- ( ( ph -> ch ) <-> ( ps -> ch ) )

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:  imor  412  ancomsimp  1416  19.43  1659  19.37  1892  dfsb3  2062  sbrim  2086  sbor  2088  sbcom2  2153  mo4f  2311  2mos  2357  neor  2686  r3al  2763  r19.23t  2821  r19.43  2866  ceqsralt  2986  ralab  3109  ralrab  3110  euind  3135  reu2  3136  rmo4  3141  reuind  3151  2reu5lem3  3155  rmo3  3273  raldifb  3484  unss  3518  ralunb  3525  inssdif0  3734  ssundif  3750  dfif2  3781  pwss  3863  ralsnsg  3897  disjsn  3924  snss  3987  raldifsni  3993  unissb  4111  intun  4148  intpr  4149  dfiin2g  4191  disjor  4264  dftr2  4375  axrep1  4392  axpweq  4457  zfpow  4459  axpow2  4460  reusv2lem4  4484  reusv2  4486  reusv7OLD  4492  raliunxp  4966  asymref2  5203  dffun2  5416  dffun4  5418  dffun5  5419  dffun7  5432  fununi  5472  dff13  5958  zfun  6362  uniex2  6364  dfom2  6467  fimaxg  7547  fiint  7576  dfsup2  7680  oemapso  7878  scottexs  8082  scott0s  8083  iscard2  8134  acnnum  8210  dfac9  8293  dfacacn  8298  kmlem4  8310  kmlem12  8318  axpowndlem3  8752  axpowndlem3OLD  8753  zfcndun  8770  zfcndpow  8771  zfcndac  8774  axgroth5  8979  grothpw  8981  axgroth6  8983  infm3  10277  raluz2  10892  nnwos  10910  ralrp  10997  lo1resb  13026  rlimresb  13027  o1resb  13028  isprm4  13756  acsfn1  14582  acsfn2  14584  lublecllem  15141  isirred2  16727  isdomn2  17293  iunocv  17948  ist1-2  18793  isnrm2  18804  dfcon2  18865  alexsubALTlem3  19463  ismbl  20851  dyadmbllem  20921  ellimc3  21196  dchrelbas2  22461  dchrelbas3  22462  legov  22892  eengtrkg  23054  isch2  24449  choc0  24552  h1dei  24776  mdsl2i  25549  xfree2  25672  spc2ed  25680  rmo3f  25703  rmo4fOLD  25704  rmo4f  25705  disjorf  25747  axextprim  27199  axunprim  27201  axpowprim  27202  untuni  27207  3orit  27218  biimpexp  27219  dfon2lem8  27450  predreseq  27487  soseq  27562  dfom5b  27790  wl-equsalcom  28219  wl-sbcom2d  28235  tsim1  28785  fphpd  29000  dford4  29223  fnwe2lem2  29249  isdomn3  29417  pm14.12  29520  raldifsnb  29969  dff14b  29991  modfsummod  30091  dfvd2an  31018  dfvd3  31027  dfvd3an  31030  uun2221  31269  uun2221p1  31270  uun2221p2  31271  bnj538  31455  bnj1101  31501  bnj1109  31503  bnj1533  31568  bnj580  31629  bnj864  31638  bnj865  31639  bnj978  31665  bnj1049  31688  bnj1090  31693  bnj1145  31707  bj-eximal  31813  bj-axrep1  31950  bj-zfpow  31957  cvlsupr3  32583  pmapglbx  33007  isltrn2N  33358  cdlemefrs29bpre0  33634