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  1486  sbrim  2012  sbal1yz  2057  sbmo  2142  mo4f  2143  moanim  2157  necon4addc  2484  necon1bddc  2491  nfraldya  2579  r3al  2588  r19.23t  2652  ceqsralt  2843  ralab  2980  ralrab  2981  euind  3007  reu2  3008  rmo4  3013  rmo3f  3017  rmo4f  3018  reuind  3025  rmo3  3138  dfdif3  3333  raldifb  3363  unss  3397  ralunb  3404  inssdif0im  3580  ssundifim  3597  raaan  3619  pwss  3693  ralsnsg  3731  ralsns  3732  disjsn  3756  snssOLD  3824  snssb  3832  unissb  3949  intun  3985  intpr  3986  dfiin2g  4029  dftr2  4215  repizf2lem  4279  axpweq  4289  zfpow  4293  axpow2  4294  zfun  4560  uniex2  4562  setindel  4665  setind  4666  elirr  4668  en2lp  4681  zfregfr  4701  tfi  4709  raliunxp  4901  dffun2  5367  dffun4  5368  dffun4f  5373  dffun7  5384  funcnveq  5424  fununi  5429  pw1dc0el  7184  fiintim  7204  addnq0mo  7778  mulnq0mo  7779  addsrmo  8074  mulsrmo  8075  prime  9695  raluz2  9929  ralrp  10026  modfsummod  12169  nnwosdc  12760  isprm4  12841  dedekindicclemicc  15623  bdcriota  16779  bj-uniex2  16812  bj-ssom  16832  exmidpeirce  16907