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  1451  sbrim  1972  sbal1yz  2017  sbmo  2101  mo4f  2102  moanim  2116  necon4addc  2434  necon1bddc  2441  nfraldya  2529  r3al  2538  r19.23t  2601  ceqsralt  2787  ralab  2920  ralrab  2921  euind  2947  reu2  2948  rmo4  2953  rmo3f  2957  rmo4f  2958  reuind  2965  rmo3  3077  dfdif3  3269  raldifb  3299  unss  3333  ralunb  3340  inssdif0im  3514  ssundifim  3530  raaan  3552  pwss  3617  ralsnsg  3655  ralsns  3656  disjsn  3680  snssOLD  3744  snssb  3751  unissb  3865  intun  3901  intpr  3902  dfiin2g  3945  dftr2  4129  repizf2lem  4190  axpweq  4200  zfpow  4204  axpow2  4205  zfun  4465  uniex2  4467  setindel  4570  setind  4571  elirr  4573  en2lp  4586  zfregfr  4606  tfi  4614  raliunxp  4803  dffun2  5264  dffun4  5265  dffun4f  5270  dffun7  5281  funcnveq  5317  fununi  5322  pw1dc0el  6967  fiintim  6985  addnq0mo  7507  mulnq0mo  7508  addsrmo  7803  mulsrmo  7804  prime  9416  raluz2  9644  ralrp  9741  modfsummod  11601  nnwosdc  12176  isprm4  12257  dedekindicclemicc  14786  bdcriota  15375  bj-uniex2  15408  bj-ssom  15428