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  395  nan  681  sbcof2  1782  sblimv  1866  sbhb  1911  sblim  1928  2sb6  1957  sbcom2v  1958  2sb6rf  1963  eu1  2022  moabs  2046  mo3h  2050  moanim  2071  2moswapdc  2087  r2alf  2450  r19.21t  2505  rspc2gv  2796  reu2  2867  reu8  2875  2reuswapdc  2883  2rmorex  2885  dfdif3  3181  ssconb  3204  ssin  3293  reldisj  3409  ssundifim  3441  ralm  3462  unissb  3761  repizf2lem  4080  elirr  4451  en2lp  4464  tfi  4491  ssrel  4622  ssrel2  4624  fncnv  5184  fun11  5185  axcaucvglemres  7700  axpre-suploc  7703  suprzclex  9142  raluz2  9367  supinfneg  9383  infsupneg  9384  infssuzex  11631  bezoutlemmain  11675  isprm2  11787  lmres  12406  limcdifap  12789