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  4145  repizf2lem  4206  axpweq  4216  zfpow  4220  axpow2  4221  zfun  4482  uniex2  4484  setindel  4587  setind  4588  elirr  4590  en2lp  4603  zfregfr  4623  tfi  4631  raliunxp  4820  dffun2  5282  dffun4  5283  dffun4f  5288  dffun7  5299  funcnveq  5338  fununi  5343  pw1dc0el  7010  fiintim  7030  addnq0mo  7562  mulnq0mo  7563  addsrmo  7858  mulsrmo  7859  prime  9474  raluz2  9702  ralrp  9799  modfsummod  11802  nnwosdc  12393  isprm4  12474  dedekindicclemicc  15137  bdcriota  15856  bj-uniex2  15889  bj-ssom  15909