Theorem imbi1i 237

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12i  238  ancomsimp  1417  sbrim  1930  sbal1yz  1977  sbmo  2059  mo4f  2060  moanim  2074  necon4addc  2379  necon1bddc  2386  nfraldya  2472  r3al  2480  r19.23t  2542  ceqsralt  2716  ralab  2848  ralrab  2849  euind  2875  reu2  2876  rmo4  2881  rmo3f  2885  rmo4f  2886  reuind  2893  rmo3  3004  dfdif3  3191  raldifb  3221  unss  3255  ralunb  3262  inssdif0im  3435  ssundifim  3451  raaan  3474  pwss  3531  ralsnsg  3568  ralsns  3569  disjsn  3593  snss  3657  unissb  3774  intun  3810  intpr  3811  dfiin2g  3854  dftr2  4036  repizf2lem  4093  axpweq  4103  zfpow  4107  axpow2  4108  zfun  4364  uniex2  4366  setindel  4461  setind  4462  elirr  4464  en2lp  4477  zfregfr  4496  tfi  4504  raliunxp  4688  dffun2  5141  dffun4  5142  dffun4f  5147  dffun7  5158  funcnveq  5194  fununi  5199  fiintim  6825  addnq0mo  7279  mulnq0mo  7280  addsrmo  7575  mulsrmo  7576  prime  9174  raluz2  9401  ralrp  9492  modfsummod  11259  isprm4  11836  dedekindicclemicc  12818  bdcriota  13252  bj-uniex2  13285  bj-ssom  13305