Theorem imbi1i 326

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

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

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 188

This theorem is referenced by:  imor  413  ancomst  453  ifpn  1430  eximal  1660  19.43  1739  19.37v  1819  19.37  2026  dfsb3  2173  sbrim  2195  sbor  2197  mo4f  2316  2mos  2352  neor  2686  r3al  2739  r3alOLD  2797  r19.23t  2836  r19.23v  2838  r19.43  2917  ceqsralt  3041  ralab  3167  ralrab  3168  euind  3193  reu2  3194  rmo4  3199  reuind  3211  2reu5lem3  3215  rmo3  3326  raldifb  3541  unss  3576  ralunb  3583  inssdif0  3800  ssundif  3817  dfif2  3849  pwss  3932  ralsnsg  3967  disjsn  3996  snss  4060  raldifsni  4066  raldifsnb  4067  unissb  4186  intun  4224  intpr  4225  dfiin2g  4268  disjor  4344  dftr2  4456  axrep1  4473  axpweq  4537  zfpow  4539  axpow2  4540  reusv2lem4  4564  reusv2  4566  raliunxp  4929  asymref2  5172  dffun2  5547  dffun4  5549  dffun5  5550  dffun7  5563  fununi  5603  fvn0ssdmfun  5965  dff13  6111  dff14b  6123  zfun  6535  uniex2  6537  dfom2  6645  fimaxg  7764  fiint  7794  dfsup2  7904  fiming  7960  oemapso  8132  scottexs  8303  scott0s  8304  iscard2  8355  acnnum  8427  dfac9  8510  dfacacn  8515  kmlem4  8527  kmlem12  8535  axpowndlem3  8968  zfcndun  8984  zfcndpow  8985  zfcndac  8988  axgroth5  9193  grothpw  9195  axgroth6  9197  addsrmo  9441  mulsrmo  9442  infm3  10512  raluz2  11152  nnwos  11170  ralrp  11265  cotr2g  12977  lo1resb  13564  rlimresb  13565  o1resb  13566  modfsummod  13790  isprm4  14570  acsfn1  15503  acsfn2  15505  lublecllem  16170  isirred2  17865  isdomn2  18459  iunocv  19179  ist1-2  20298  isnrm2  20309  dfcon2  20369  alexsubALTlem3  20999  ismbl  22415  dyadmbllem  22492  ellimc3  22769  dchrelbas2  24100  dchrelbas3  24101  isch2  26811  choc0  26914  h1dei  27138  mdsl2i  27910  rmo3f  28066  rmo4fOLD  28067  rmo4f  28068  disjorf  28128  bnj538OLD  29495  bnj1101  29541  bnj1109  29543  bnj1533  29608  bnj580  29669  bnj864  29678  bnj865  29679  bnj978  29705  bnj1049  29728  bnj1090  29733  bnj1145  29747  axextprim  30273  axunprim  30275  axpowprim  30276  untuni  30281  3orit  30292  biimpexp  30293  dfon2lem8  30380  soseq  30436  dfom5b  30621  bj-axrep1  31310  bj-zfpow  31317  rdgeqoa  31674  wl-equsalcom  31776  poimirlem25  31866  poimirlem30  31871  tsim1  32273  cvlsupr3  32816  pmapglbx  33240  isltrn2N  33591  cdlemefrs29bpre0  33869  fphpd  35565  dford4  35791  fnwe2lem2  35816  isdomn3  35988  ifpidg  36042  ifpid1g  36045  ifpor123g  36059  undmrnresiss  36117  elintima  36152  df3or2  36267  dfhe3  36277  dffrege76  36442  dffrege115  36481  frege131  36497  pm14.12  36679  dfvd2an  36860  dfvd3  36869  dfvd3an  36872  uun2221  37110  uun2221p1  37111  uun2221p2  37112  disjinfi  37366  fsummulc1f  37525  fsumiunss  37532  dvmptmulf  37689  dvnmul  37695  dvmptfprodlem  37696  dvnprodlem2  37699  sge0ltfirpmpt2  38113  hoidmv1le  38257  hoidmvle  38263  aacllem  40127