Theorem imbi2i 226

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12i  239  anidmdbi  398  nan  693  sbcof2  1824  sblimv  1909  sbhb  1959  sblim  1976  2sb6  2003  sbcom2v  2004  2sb6rf  2009  eu1  2070  moabs  2094  mo3h  2098  moanim  2119  2moswapdc  2135  r2alf  2514  r19.21t  2572  rspc2gv  2880  reu2  2952  reu8  2960  2reuswapdc  2968  2rmorex  2970  dfdif3  3273  ssconb  3296  ssin  3385  reldisj  3502  ssundifim  3534  ralm  3554  unissb  3869  repizf2lem  4194  elirr  4577  en2lp  4590  tfi  4618  ssrel  4751  ssrel2  4753  fncnv  5324  fun11  5325  axcaucvglemres  7966  axpre-suploc  7969  suprzclex  9424  raluz2  9653  supinfneg  9669  infsupneg  9670  infssuzex  10323  bezoutlemmain  12165  isprm2  12285  lmres  14484  ivthdich  14889  limcdifap  14898