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  1975  sbal1yz  2020  sbmo  2104  mo4f  2105  moanim  2119  necon4addc  2437  necon1bddc  2444  nfraldya  2532  r3al  2541  r19.23t  2604  ceqsralt  2790  ralab  2924  ralrab  2925  euind  2951  reu2  2952  rmo4  2957  rmo3f  2961  rmo4f  2962  reuind  2969  rmo3  3081  dfdif3  3274  raldifb  3304  unss  3338  ralunb  3345  inssdif0im  3519  ssundifim  3535  raaan  3557  pwss  3622  ralsnsg  3660  ralsns  3661  disjsn  3685  snssOLD  3749  snssb  3756  unissb  3870  intun  3906  intpr  3907  dfiin2g  3950  dftr2  4134  repizf2lem  4195  axpweq  4205  zfpow  4209  axpow2  4210  zfun  4470  uniex2  4472  setindel  4575  setind  4576  elirr  4578  en2lp  4591  zfregfr  4611  tfi  4619  raliunxp  4808  dffun2  5269  dffun4  5270  dffun4f  5275  dffun7  5286  funcnveq  5322  fununi  5327  pw1dc0el  6981  fiintim  7001  addnq0mo  7531  mulnq0mo  7532  addsrmo  7827  mulsrmo  7828  prime  9442  raluz2  9670  ralrp  9767  modfsummod  11640  nnwosdc  12231  isprm4  12312  dedekindicclemicc  14952  bdcriota  15613  bj-uniex2  15646  bj-ssom  15666