Theorem imbi2i 304

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 11	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.74i 237	1 |- ( ( ch -> ph ) <-> ( ch -> ps ) )

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

This theorem is referenced by:  imbi12i  317  iman  414  pm4.14  562  nan  564  pm5.32  618  anidmdbi  628  imimorb  848  pm5.6  879  exp3acom23g  1377  19.36  1888  sblim  2117  sban  2118  sbhb  2156  2sb6  2162  2sb6rf  2168  eu1  2275  moabs  2298  moanim  2310  2eu6  2339  r2alf  2701  r19.21t  2751  r19.35  2815  reu2  3082  reu8  3090  2reu5lem3  3101  ssconb  3440  ssin  3523  difin  3538  reldisj  3631  ssundif  3671  pwpw0  3906  pwsnALT  3970  unissb  4005  moabex  4382  dffr2  4507  dfepfr  4527  ssrel  4923  ssrel2  4925  dffr3  5195  fncnv  5474  fun11  5475  dff13  5963  marypha2lem3  7400  dfsup2  7405  wemapso2lem  7475  inf2  7534  axinf2  7551  aceq1  7954  aceq0  7955  kmlem14  7999  dfackm  8002  zfac  8296  ac6n  8321  zfcndrep  8445  zfcndac  8450  axgroth6  8659  axgroth4  8663  grothprim  8665  prime  10306  raluz2  10482  rpnnen2  12780  isprm2  13042  isprm4  13044  pgpfac1  15593  pgpfac  15597  isirred2  15761  isclo2  17107  lmres  17318  ist1-2  17365  is1stc2  17458  alexsubALTlem3  18033  itg2cn  19608  ellimc3  19719  plydivex  20167  vieta1  20182  dchrelbas2  20974  nmobndseqi  22233  nmobndseqiOLD  22234  cvnbtwn3  23744  elat2  23796  funcnvmptOLD  24035  isarchi2  24208  axinfprim  25108  dfon2lem9  25361  dffr4  25396  dffun10  25667  df3nandALT1  26050  df3nandALT2  26051  elicc3  26210  filnetlem4  26300  raldifsni  26624  dford4  26990  pm10.541  27430  pm13.196a  27482  2sbc6g  27483  rmoanim  27824  sbidd-misc  28176  impexp3a  28307  bnj1098  28860  bnj1533  28929  bnj121  28947  bnj124  28948  bnj130  28951  bnj153  28957  bnj207  28958  bnj611  28995  bnj864  28999  bnj865  29000  bnj1000  29018  bnj978  29026  bnj1021  29041  bnj1047  29048  bnj1049  29049  bnj1090  29054  bnj1110  29057  bnj1128  29065  bnj1145  29068  bnj1171  29075  bnj1172  29076  bnj1174  29078  bnj1176  29080  bnj1280  29095  sblimNEW7  29272  sbanNEW7  29273  sbhbwAUX7  29308  2sb6NEW7  29311  sbhbOLD7  29444  2sb6rfOLD7  29447  lcvnbtwn3  29511  isat3  29790  cdleme25cv  30840  cdlemefrs29bpre0  30878  cdlemk35  31394

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178