Theorem imbi1i 325

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-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  ancomst  452  19.43  1660  19.37  1894  dfsb3  2065  sbrim  2088  sbor  2090  sbcom2  2151  mo4f  2316  2mos  2363  neor  2699  r3al  2776  r19.23t  2834  r19.43  2879  ceqsralt  2999  ralab  3123  ralrab  3124  euind  3149  reu2  3150  rmo4  3155  reuind  3165  2reu5lem3  3169  rmo3  3288  raldifb  3499  unss  3533  ralunb  3540  inssdif0  3749  ssundif  3765  dfif2  3796  pwss  3878  ralsnsg  3912  disjsn  3939  snss  4002  raldifsni  4008  unissb  4126  intun  4163  intpr  4164  dfiin2g  4206  disjor  4279  dftr2  4390  axrep1  4407  axpweq  4472  zfpow  4474  axpow2  4475  reusv2lem4  4499  reusv2  4501  reusv7OLD  4507  raliunxp  4982  asymref2  5218  dffun2  5431  dffun4  5433  dffun5  5434  dffun7  5447  fununi  5487  dff13  5974  zfun  6376  uniex2  6378  dfom2  6481  fimaxg  7562  fiint  7591  dfsup2  7695  oemapso  7893  scottexs  8097  scott0s  8098  iscard2  8149  acnnum  8225  dfac9  8308  dfacacn  8313  kmlem4  8325  kmlem12  8333  axpowndlem3  8767  axpowndlem3OLD  8768  zfcndun  8785  zfcndpow  8786  zfcndac  8789  axgroth5  8994  grothpw  8996  axgroth6  8998  infm3  10292  raluz2  10907  nnwos  10925  ralrp  11012  lo1resb  13045  rlimresb  13046  o1resb  13047  isprm4  13776  acsfn1  14602  acsfn2  14604  lublecllem  15161  isirred2  16796  isdomn2  17374  iunocv  18109  ist1-2  18954  isnrm2  18965  dfcon2  19026  alexsubALTlem3  19624  ismbl  21012  dyadmbllem  21082  ellimc3  21357  dchrelbas2  22579  dchrelbas3  22580  legov  23019  eengtrkg  23234  isch2  24629  choc0  24732  h1dei  24956  mdsl2i  25729  xfree2  25852  spc2ed  25860  rmo3f  25882  rmo4fOLD  25883  rmo4f  25884  disjorf  25926  axextprim  27355  axunprim  27357  axpowprim  27358  untuni  27363  3orit  27374  biimpexp  27375  dfon2lem8  27606  predreseq  27643  soseq  27718  dfom5b  27946  wl-equsalcom  28374  wl-sbcom2d  28390  tsim1  28944  fphpd  29158  dford4  29381  fnwe2lem2  29407  isdomn3  29575  pm14.12  29678  raldifsnb  30126  dff14b  30148  modfsummod  30248  dfvd2an  31298  dfvd3  31307  dfvd3an  31310  uun2221  31549  uun2221p1  31550  uun2221p2  31551  bnj538  31735  bnj1101  31781  bnj1109  31783  bnj1533  31848  bnj580  31909  bnj864  31918  bnj865  31919  bnj978  31945  bnj1049  31968  bnj1090  31973  bnj1145  31987  bj-ifn  32095  bj-eximal  32133  bj-axrep1  32312  bj-zfpow  32319  cvlsupr3  32992  pmapglbx  33416  isltrn2N  33767  cdlemefrs29bpre0  34043