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  682  sbcof2  1790  sblimv  1874  sbhb  1920  sblim  1937  2sb6  1964  sbcom2v  1965  2sb6rf  1970  eu1  2031  moabs  2055  mo3h  2059  moanim  2080  2moswapdc  2096  r2alf  2474  r19.21t  2532  rspc2gv  2828  reu2  2900  reu8  2908  2reuswapdc  2916  2rmorex  2918  dfdif3  3217  ssconb  3240  ssin  3329  reldisj  3445  ssundifim  3477  ralm  3498  unissb  3802  repizf2lem  4121  elirr  4498  en2lp  4511  tfi  4539  ssrel  4671  ssrel2  4673  fncnv  5233  fun11  5234  axcaucvglemres  7802  axpre-suploc  7805  suprzclex  9245  raluz2  9473  supinfneg  9489  infsupneg  9490  infssuzex  11817  bezoutlemmain  11862  isprm2  11974  lmres  12608  limcdifap  12991