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  1369  sbrim  1871  sbal1yz  1918  sbmo  2000  mo4f  2001  moanim  2015  necon4addc  2315  necon1bddc  2322  nfraldya  2400  r3al  2408  r19.23t  2467  ceqsralt  2626  ralab  2752  ralrab  2753  euind  2779  reu2  2780  rmo4  2785  reuind  2795  rmo3  2905  raldifb  3112  unss  3146  ralunb  3153  inssdif0im  3311  ssundifim  3326  raaan  3347  pwss  3397  ralsnsg  3430  ralsns  3431  disjsn  3454  snss  3516  unissb  3631  intun  3667  intpr  3668  dfiin2g  3711  dftr2  3877  repizf2lem  3935  axpweq  3945  zfpow  3949  axpow2  3950  zfun  4189  uniex2  4191  setindel  4281  setind  4282  elirr  4284  en2lp  4297  zfregfr  4316  tfi  4323  raliunxp  4495  dffun2  4932  dffun4  4933  dffun4f  4938  dffun7  4948  funcnveq  4982  fununi  4987  addnq0mo  6637  mulnq0mo  6638  addsrmo  6920  mulsrmo  6921  prime  8446  raluz2  8667  ralrp  8755  isprm4  10501  bdcriota  10674  bj-uniex2  10707  bj-ssom  10731