Theorem imbi1i 236

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 234	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ch ) <-> ( ps -> ch ) ) )
3	1, 2	ax-mp 7	1 |- ( ( ph -> ch ) <-> ( ps -> ch ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  imbi12i  237  ancomsimp  1372  sbrim  1875  sbal1yz  1922  sbmo  2004  mo4f  2005  moanim  2019  necon4addc  2321  necon1bddc  2328  nfraldya  2408  r3al  2416  r19.23t  2475  ceqsralt  2640  ralab  2766  ralrab  2767  euind  2793  reu2  2794  rmo4  2799  reuind  2809  rmo3  2919  dfdif3  3099  raldifb  3129  unss  3163  ralunb  3170  inssdif0im  3338  ssundifim  3353  raaan  3375  pwss  3430  ralsnsg  3463  ralsns  3464  disjsn  3487  snss  3549  unissb  3666  intun  3702  intpr  3703  dfiin2g  3746  dftr2  3912  repizf2lem  3970  axpweq  3980  zfpow  3984  axpow2  3985  zfun  4234  uniex2  4236  setindel  4326  setind  4327  elirr  4329  en2lp  4342  zfregfr  4361  tfi  4369  raliunxp  4544  dffun2  4988  dffun4  4989  dffun4f  4994  dffun7  5004  funcnveq  5039  fununi  5044  addnq0mo  6943  mulnq0mo  6944  addsrmo  7226  mulsrmo  7227  prime  8771  raluz2  8992  ralrp  9080  isprm4  10968  bdcriota  11204  bj-uniex2  11237  bj-ssom  11261