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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 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  1428  sbrim  1944  sbal1yz  1989  sbmo  2073  mo4f  2074  moanim  2088  necon4addc  2406  necon1bddc  2413  nfraldya  2501  r3al  2510  r19.23t  2573  ceqsralt  2753  ralab  2886  ralrab  2887  euind  2913  reu2  2914  rmo4  2919  rmo3f  2923  rmo4f  2924  reuind  2931  rmo3  3042  dfdif3  3232  raldifb  3262  unss  3296  ralunb  3303  inssdif0im  3476  ssundifim  3492  raaan  3515  pwss  3575  ralsnsg  3613  ralsns  3614  disjsn  3638  snss  3702  unissb  3819  intun  3855  intpr  3856  dfiin2g  3899  dftr2  4082  repizf2lem  4140  axpweq  4150  zfpow  4154  axpow2  4155  zfun  4412  uniex2  4414  setindel  4515  setind  4516  elirr  4518  en2lp  4531  zfregfr  4551  tfi  4559  raliunxp  4745  dffun2  5198  dffun4  5199  dffun4f  5204  dffun7  5215  funcnveq  5251  fununi  5256  pw1dc0el  6877  fiintim  6894  addnq0mo  7388  mulnq0mo  7389  addsrmo  7684  mulsrmo  7685  prime  9290  raluz2  9517  ralrp  9611  modfsummod  11399  nnwosdc  11972  isprm4  12051  dedekindicclemicc  13250  bdcriota  13765  bj-uniex2  13798  bj-ssom  13818