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  1460  sbrim  1984  sbal1yz  2029  sbmo  2113  mo4f  2114  moanim  2128  necon4addc  2446  necon1bddc  2453  nfraldya  2541  r3al  2550  r19.23t  2613  ceqsralt  2799  ralab  2933  ralrab  2934  euind  2960  reu2  2961  rmo4  2966  rmo3f  2970  rmo4f  2971  reuind  2978  rmo3  3090  dfdif3  3283  raldifb  3313  unss  3347  ralunb  3354  inssdif0im  3528  ssundifim  3544  raaan  3566  pwss  3632  ralsnsg  3670  ralsns  3671  disjsn  3695  snssOLD  3759  snssb  3766  unissb  3880  intun  3916  intpr  3917  dfiin2g  3960  dftr2  4144  repizf2lem  4205  axpweq  4215  zfpow  4219  axpow2  4220  zfun  4481  uniex2  4483  setindel  4586  setind  4587  elirr  4589  en2lp  4602  zfregfr  4622  tfi  4630  raliunxp  4819  dffun2  5281  dffun4  5282  dffun4f  5287  dffun7  5298  funcnveq  5337  fununi  5342  pw1dc0el  7008  fiintim  7028  addnq0mo  7560  mulnq0mo  7561  addsrmo  7856  mulsrmo  7857  prime  9472  raluz2  9700  ralrp  9797  modfsummod  11769  nnwosdc  12360  isprm4  12441  dedekindicclemicc  15104  bdcriota  15823  bj-uniex2  15856  bj-ssom  15876