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  696  sbcof2  1856  sblimv  1941  sbhb  1991  sblim  2008  2sb6  2035  sbcom2v  2036  2sb6rf  2041  eu1  2102  moabs  2127  mo3h  2131  moanim  2152  2moswapdc  2168  r2alf  2547  r19.21t  2605  rspc2gv  2919  reu2  2991  reu8  2999  2reuswapdc  3007  2rmorex  3009  dfdif3  3314  ssconb  3337  ssin  3426  reldisj  3543  ssundifim  3575  ralm  3595  unissb  3918  repizf2lem  4245  elirr  4633  en2lp  4646  tfi  4674  ssrel  4807  ssrel2  4809  fncnv  5387  fun11  5388  axcaucvglemres  8086  axpre-suploc  8089  suprzclex  9545  raluz2  9774  supinfneg  9790  infsupneg  9791  infssuzex  10453  bezoutlemmain  12519  isprm2  12639  lmres  14922  ivthdich  15327  limcdifap  15336