Theorem imbi2i 215

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 169	1 |- ((ch -> ph) <-> (ch -> ps))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  imbi12i  228  anidmdbi  378  nan  625  sbcof2  1688  sblimv  1771  sbhb  1813  sblim  1828  2sb6  1857  sbcom2v  1858  2sb6rf  1863  eu1  1922  moabs  1946  mo3h  1950  moanim  1971  2moswapdc  1987  r2alf  2335  r19.21t  2388  reu2  2723  reu8  2731  2reuswapdc  2737  2rmorex  2739  ssconb  3070  ssin  3153  reldisj  3265  ssundifim  3300  ralm  3319  unissb  3601  repizf2lem  3905  elirr  4224  en2lp  4232  tfi  4248  ssrel  4371  ssrel2  4373  fncnv  4908  fun11  4909  raluz2  8298