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  1968  sbal1yz  2013  sbmo  2097  mo4f  2098  moanim  2112  necon4addc  2430  necon1bddc  2437  nfraldya  2525  r3al  2534  r19.23t  2597  ceqsralt  2779  ralab  2912  ralrab  2913  euind  2939  reu2  2940  rmo4  2945  rmo3f  2949  rmo4f  2950  reuind  2957  rmo3  3069  dfdif3  3260  raldifb  3290  unss  3324  ralunb  3331  inssdif0im  3505  ssundifim  3521  raaan  3544  pwss  3609  ralsnsg  3647  ralsns  3648  disjsn  3672  snssOLD  3736  snssb  3743  unissb  3857  intun  3893  intpr  3894  dfiin2g  3937  dftr2  4121  repizf2lem  4182  axpweq  4192  zfpow  4196  axpow2  4197  zfun  4455  uniex2  4457  setindel  4558  setind  4559  elirr  4561  en2lp  4574  zfregfr  4594  tfi  4602  raliunxp  4789  dffun2  5248  dffun4  5249  dffun4f  5254  dffun7  5265  funcnveq  5301  fununi  5306  pw1dc0el  6943  fiintim  6961  addnq0mo  7481  mulnq0mo  7482  addsrmo  7777  mulsrmo  7778  prime  9387  raluz2  9615  ralrp  9711  modfsummod  11507  nnwosdc  12081  isprm4  12162  dedekindicclemicc  14595  bdcriota  15121  bj-uniex2  15154  bj-ssom  15174