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-1 5  ax-2 6  ax-mp 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  393  nan  664  sbcof2  1762  sblimv  1846  sbhb  1889  sblim  1904  2sb6  1933  sbcom2v  1934  2sb6rf  1939  eu1  1998  moabs  2022  mo3h  2026  moanim  2047  2moswapdc  2063  r2alf  2424  r19.21t  2479  rspc2gv  2769  reu2  2839  reu8  2847  2reuswapdc  2855  2rmorex  2857  dfdif3  3150  ssconb  3173  ssin  3262  reldisj  3378  ssundifim  3410  ralm  3431  unissb  3730  repizf2lem  4043  elirr  4414  en2lp  4427  tfi  4454  ssrel  4585  ssrel2  4587  fncnv  5145  fun11  5146  axcaucvglemres  7628  suprzclex  9047  raluz2  9270  supinfneg  9286  infsupneg  9287  infssuzex  11484  bezoutlemmain  11526  isprm2  11638  lmres  12253  limcdifap  12581