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  1798  sblimv  1882  sbhb  1928  sblim  1945  2sb6  1972  sbcom2v  1973  2sb6rf  1978  eu1  2039  moabs  2063  mo3h  2067  moanim  2088  2moswapdc  2104  r2alf  2483  r19.21t  2541  rspc2gv  2842  reu2  2914  reu8  2922  2reuswapdc  2930  2rmorex  2932  dfdif3  3232  ssconb  3255  ssin  3344  reldisj  3460  ssundifim  3492  ralm  3513  unissb  3819  repizf2lem  4140  elirr  4518  en2lp  4531  tfi  4559  ssrel  4692  ssrel2  4694  fncnv  5254  fun11  5255  axcaucvglemres  7840  axpre-suploc  7843  suprzclex  9289  raluz2  9517  supinfneg  9533  infsupneg  9534  infssuzex  11882  bezoutlemmain  11931  isprm2  12049  lmres  12888  limcdifap  13271