Theorem imbi2i 312

Description: Introduce an antecedent to both sides of a logical equivalence. This and the next three rules are useful for building up wff's around a definition, in order to make use of the definition. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)

Hypothesis

Ref	Expression
imbi2i.1	|- ( ph <-> ps )

Assertion

Ref	Expression
imbi2i	|- ( ( ch -> ph ) <-> ( ch -> ps ) )

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		imbi2i.1	. . 3 |- ( ph <-> ps )
2	1	a1i 11	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.74i 245	1 |- ( ( ch -> ph ) <-> ( ch -> ps ) )

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

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

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  iman  424  pm4.14  578  nan  580  pm5.32  636  anidmdbi  646  imimorb  872  pm5.6  903  19.36  1892  sblim  2089  sban  2091  sbhb  2143  2sb6  2150  2sb6rfOLD  2162  mo2v  2260  mo2vOLD  2261  mo2vOLDOLD  2262  moabs  2288  eu1  2303  eu1OLD  2304  moanimOLD  2333  2eu6OLD  2372  r2alf  2769  r19.21t  2820  r19.35  2886  reu2  3166  reu8  3174  2reu5lem3  3185  ssconb  3508  ssin  3591  difin  3606  reldisj  3741  ssundif  3781  raldifsni  4024  pwpw0  4040  pwsnALT  4105  unissb  4142  moabex  4570  dffr2  4704  dfepfr  4724  ssrel  4947  ssrel2  4949  dffr3  5220  fncnv  5501  fun11  5502  dff13  5990  marypha2lem3  7706  dfsup2  7711  wemapsolem  7783  inf2  7848  axinf2  7865  aceq1  8306  aceq0  8307  kmlem14  8351  dfackm  8354  zfac  8648  ac6n  8673  zfcndrep  8800  zfcndac  8805  axgroth6  9014  axgroth4  9018  grothprim  9020  prime  10741  raluz2  10923  rpnnen2  13527  isprm2  13790  isprm4  13792  pgpfac1  16600  pgpfac  16604  isirred2  16812  isclo2  18711  lmres  18923  ist1-2  18970  is1stc2  19065  alexsubALTlem3  19640  itg2cn  21260  ellimc3  21373  plydivex  21782  vieta1  21797  dchrelbas2  22595  ecgrtg  23248  nmobndseqi  24198  nmobndseqiOLD  24199  cvnbtwn3  25711  elat2  25763  ssrelf  25964  funcnvmptOLD  26005  resf1o  26049  isarchi2  26221  archiabl  26234  orngsqr  26291  signstfvneq0  26992  axinfprim  27376  dfon2lem9  27623  dffr4  27662  dffun10  27964  df3nandALT1  28262  df3nandALT2  28263  elicc3  28535  filnetlem4  28625  sbcalf  28943  sbcexf  28944  scott0f  29004  dford4  29401  pm10.541  29642  pm13.196a  29691  2sbc6g  29692  rmoanim  30026  fsuppmapnn0ub  30819  pmatcollpw2lem  30928  ldepslinc  31074  sbidd-misc  31077  expcomdg  31227  impexpd  31241  bnj1098  31800  bnj1533  31868  bnj121  31886  bnj124  31887  bnj130  31890  bnj153  31896  bnj207  31897  bnj611  31934  bnj864  31938  bnj865  31939  bnj1000  31957  bnj978  31965  bnj1021  31980  bnj1047  31987  bnj1049  31988  bnj1090  31993  bnj1110  31996  bnj1128  32004  bnj1145  32007  bnj1171  32014  bnj1172  32015  bnj1174  32017  bnj1176  32019  bnj1280  32034  bj-alimex  32172  bj-sbnf  32370  lcvnbtwn3  32696  isat3  32975  cdleme25cv  34025  cdlemefrs29bpre0  34063  cdlemk35  34579