Theorem imbi2i 224

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  imbi12i  237  anidmdbi  390  nan  659  sbcof2  1732  sblimv  1816  sbhb  1858  sblim  1873  2sb6  1902  sbcom2v  1903  2sb6rf  1908  eu1  1967  moabs  1991  mo3h  1995  moanim  2016  2moswapdc  2032  r2alf  2384  r19.21t  2437  rspc2gv  2713  reu2  2781  reu8  2789  2reuswapdc  2795  2rmorex  2797  ssconb  3106  ssin  3195  reldisj  3302  ssundifim  3333  ralm  3353  unissb  3639  repizf2lem  3943  elirr  4292  en2lp  4305  tfi  4331  ssrel  4454  ssrel2  4456  fncnv  4996  fun11  4997  axcaucvglemres  7127  suprzclex  8526  raluz2  8748  supinfneg  8764  infsupneg  8765  infssuzex  10489  bezoutlemmain  10531  isprm2  10643