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  1416  sbrim  1929  sbal1yz  1976  sbmo  2058  mo4f  2059  moanim  2073  necon4addc  2378  necon1bddc  2385  nfraldya  2469  r3al  2477  r19.23t  2539  ceqsralt  2713  ralab  2844  ralrab  2845  euind  2871  reu2  2872  rmo4  2877  rmo3f  2881  rmo4f  2882  reuind  2889  rmo3  3000  dfdif3  3186  raldifb  3216  unss  3250  ralunb  3257  inssdif0im  3430  ssundifim  3446  raaan  3469  pwss  3526  ralsnsg  3561  ralsns  3562  disjsn  3585  snss  3649  unissb  3766  intun  3802  intpr  3803  dfiin2g  3846  dftr2  4028  repizf2lem  4085  axpweq  4095  zfpow  4099  axpow2  4100  zfun  4356  uniex2  4358  setindel  4453  setind  4454  elirr  4456  en2lp  4469  zfregfr  4488  tfi  4496  raliunxp  4680  dffun2  5133  dffun4  5134  dffun4f  5139  dffun7  5150  funcnveq  5186  fununi  5191  fiintim  6817  addnq0mo  7255  mulnq0mo  7256  addsrmo  7551  mulsrmo  7552  prime  9150  raluz2  9374  ralrp  9463  modfsummod  11227  isprm4  11800  dedekindicclemicc  12779  bdcriota  13081  bj-uniex2  13114  bj-ssom  13134