Theorem imbi1i 238

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12i  239  ancomsimp  1461  sbrim  1985  sbal1yz  2030  sbmo  2115  mo4f  2116  moanim  2130  necon4addc  2448  necon1bddc  2455  nfraldya  2543  r3al  2552  r19.23t  2615  ceqsralt  2804  ralab  2940  ralrab  2941  euind  2967  reu2  2968  rmo4  2973  rmo3f  2977  rmo4f  2978  reuind  2985  rmo3  3098  dfdif3  3291  raldifb  3321  unss  3355  ralunb  3362  inssdif0im  3536  ssundifim  3552  raaan  3574  pwss  3642  ralsnsg  3680  ralsns  3681  disjsn  3705  snssOLD  3770  snssb  3777  unissb  3894  intun  3930  intpr  3931  dfiin2g  3974  dftr2  4160  repizf2lem  4221  axpweq  4231  zfpow  4235  axpow2  4236  zfun  4499  uniex2  4501  setindel  4604  setind  4605  elirr  4607  en2lp  4620  zfregfr  4640  tfi  4648  raliunxp  4837  dffun2  5300  dffun4  5301  dffun4f  5306  dffun7  5317  funcnveq  5356  fununi  5361  pw1dc0el  7034  fiintim  7054  addnq0mo  7595  mulnq0mo  7596  addsrmo  7891  mulsrmo  7892  prime  9507  raluz2  9735  ralrp  9832  modfsummod  11884  nnwosdc  12475  isprm4  12556  dedekindicclemicc  15219  bdcriota  16018  bj-uniex2  16051  bj-ssom  16071