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 7	1 |- ( ( ph -> ch ) <-> ( ps -> ch ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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  1384  sbrim  1890  sbal1yz  1937  sbmo  2019  mo4f  2020  moanim  2034  necon4addc  2337  necon1bddc  2344  nfraldya  2428  r3al  2436  r19.23t  2498  ceqsralt  2668  ralab  2797  ralrab  2798  euind  2824  reu2  2825  rmo4  2830  rmo3f  2834  rmo4f  2835  reuind  2842  rmo3  2952  dfdif3  3133  raldifb  3163  unss  3197  ralunb  3204  inssdif0im  3377  ssundifim  3393  raaan  3416  pwss  3473  ralsnsg  3508  ralsns  3509  disjsn  3532  snss  3596  unissb  3713  intun  3749  intpr  3750  dfiin2g  3793  dftr2  3968  repizf2lem  4025  axpweq  4035  zfpow  4039  axpow2  4040  zfun  4294  uniex2  4296  setindel  4391  setind  4392  elirr  4394  en2lp  4407  zfregfr  4426  tfi  4434  raliunxp  4618  dffun2  5069  dffun4  5070  dffun4f  5075  dffun7  5086  funcnveq  5122  fununi  5127  fiintim  6746  addnq0mo  7156  mulnq0mo  7157  addsrmo  7439  mulsrmo  7440  prime  9002  raluz2  9224  ralrp  9312  modfsummod  11066  isprm4  11593  bdcriota  12662  bj-uniex2  12695  bj-ssom  12719