Theorem imbi2i 225

Description: Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)

Hypothesis

Ref	Expression
bi.a	|- ( ph <-> ps )

Assertion

Ref	Expression
imbi2i	|- ( ( ch -> ph ) <-> ( ch -> ps ) )

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		bi.a	. . 3 |- ( ph <-> ps )
2	1	a1i 9	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.74i 179	1 |- ( ( ch -> ph ) <-> ( ch -> ps ) )

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  anidmdbi  396  nan  687  sbcof2  1803  sblimv  1887  sbhb  1933  sblim  1950  2sb6  1977  sbcom2v  1978  2sb6rf  1983  eu1  2044  moabs  2068  mo3h  2072  moanim  2093  2moswapdc  2109  r2alf  2487  r19.21t  2545  rspc2gv  2846  reu2  2918  reu8  2926  2reuswapdc  2934  2rmorex  2936  dfdif3  3237  ssconb  3260  ssin  3349  reldisj  3466  ssundifim  3498  ralm  3519  unissb  3826  repizf2lem  4147  elirr  4525  en2lp  4538  tfi  4566  ssrel  4699  ssrel2  4701  fncnv  5264  fun11  5265  axcaucvglemres  7861  axpre-suploc  7864  suprzclex  9310  raluz2  9538  supinfneg  9554  infsupneg  9555  infssuzex  11904  bezoutlemmain  11953  isprm2  12071  lmres  13042  limcdifap  13425