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  eximal  1600  19.43  1678  19.37v  1753  19.37  1950  dfsb3  2099  sbrim  2121  sbor  2123  mo4f  2320  2mos  2359  neor  2765  r3al  2821  r3alOLD  2879  r19.23t  2919  r19.23v  2921  r19.43  2997  ceqsralt  3117  ralab  3244  ralrab  3245  euind  3270  reu2  3271  rmo4  3276  reuind  3287  2reu5lem3  3291  rmo3  3412  raldifb  3626  unss  3660  ralunb  3667  inssdif0  3877  ssundif  3893  dfif2  3924  pwss  4008  ralsnsg  4042  disjsn  4071  snss  4135  raldifsni  4141  raldifsnb  4142  unissb  4262  intun  4300  intpr  4301  dfiin2g  4344  disjor  4417  dftr2  4528  axrep1  4545  axpweq  4610  zfpow  4612  axpow2  4613  reusv2lem4  4637  reusv2  4639  reusv7OLD  4645  raliunxp  5128  asymref2  5370  dffun2  5584  dffun4  5586  dffun5  5587  dffun7  5600  fununi  5640  fvn0ssdmfun  6003  dff13  6147  dff14b  6159  zfun  6574  uniex2  6576  dfom2  6683  fimaxg  7765  fiint  7795  dfsup2  7900  oemapso  8099  scottexs  8303  scott0s  8304  iscard2  8355  acnnum  8431  dfac9  8514  dfacacn  8519  kmlem4  8531  kmlem12  8539  axpowndlem3  8973  axpowndlem3OLD  8974  zfcndun  8991  zfcndpow  8992  zfcndac  8995  axgroth5  9200  grothpw  9202  axgroth6  9204  addsrmo  9448  mulsrmo  9449  infm3  10503  raluz2  11134  nnwos  11153  ralrp  11242  lo1resb  13361  rlimresb  13362  o1resb  13363  modfsummod  13582  isprm4  14099  acsfn1  14930  acsfn2  14932  lublecllem  15487  isirred2  17218  isdomn2  17816  iunocv  18579  ist1-2  19714  isnrm2  19725  dfcon2  19786  alexsubALTlem3  20415  ismbl  21803  dyadmbllem  21874  ellimc3  22149  dchrelbas2  23377  dchrelbas3  23378  isch2  26006  choc0  26109  h1dei  26333  mdsl2i  27106  rmo3f  27259  rmo4fOLD  27260  rmo4f  27261  disjorf  27305  axextprim  28939  axunprim  28941  axpowprim  28942  untuni  28947  3orit  28958  biimpexp  28959  dfon2lem8  29190  predreseq  29227  soseq  29302  dfom5b  29530  wl-equsalcom  29963  tsim1  30505  fphpd  30718  dford4  30939  fnwe2lem2  30965  isdomn3  31133  pm14.12  31275  dfvd2an  33067  dfvd3  33076  dfvd3an  33079  uun2221  33318  uun2221p1  33319  uun2221p2  33320  bnj538  33504  bnj1101  33550  bnj1109  33552  bnj1533  33617  bnj580  33678  bnj864  33687  bnj865  33688  bnj978  33714  bnj1049  33737  bnj1090  33742  bnj1145  33756  bj-ifn  33869  bj-axrep1  34086  bj-zfpow  34093  cvlsupr3  34771  pmapglbx  35195  isltrn2N  35546  cdlemefrs29bpre0  35824  cotr2g  37441