Theorem imbi2i 303

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 10	. 2 |- (ch -> (ph <-> ps))
3	2	pm5.74i 236	1 |- ((ch -> ph) <-> (ch -> ps))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  imbi12i  316  iman  413  pm4.14  561  nan  563  pm5.32  617  anidmdbi  627  imimorb  847  pm5.6  878  exp3acom23g  1371  19.36  1871  sblim  2068  sban  2069  sbhb  2107  2sb6  2113  2sb6rf  2118  eu1  2225  moabs  2248  moanim  2260  2eu6  2289  axi12  2333  r2alf  2650  r19.21t  2700  r19.35  2759  reu2  3025  reu8  3033  2reu5lem3  3044  ssconb  3400  ssin  3478  difin  3493  reldisj  3595  ssundif  3634  pwpw0  3856  pwsnALT  3883  unissb  3922  evenodddisj  4517  tfinnn  4535  fncnv  5159  fun11  5160  dff13  5472  frds  5936  ncssfin  6152  sbth  6207  spacind  6288