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  875  pm5.6  910  19.36  1913  19.36v  1935  sblim  2112  sban  2114  sbhb  2165  2sb6  2172  2sb6rfOLD  2184  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  moabs  2310  eu1  2325  eu1OLD  2326  moanimOLD  2355  2eu6OLD  2394  r2allem  2839  r2alfOLD  2841  r3al  2844  r19.21t  2861  r19.21tOLD  2862  r19.21v  2869  ralbii  2895  r19.35  3008  reu2  3291  reu8  3299  2reu5lem3  3311  ssconb  3637  ssin  3720  difin  3735  reldisj  3870  ssundif  3910  raldifsni  4157  pwpw0  4175  pwsnALT  4240  unissb  4277  moabex  4706  dffr2  4844  dfepfr  4864  ssrel  5091  ssrel2  5093  dffr3  5369  fncnv  5652  fun11  5653  dff13  6155  marypha2lem3  7898  dfsup2  7903  wemapsolem  7976  inf2  8041  axinf2  8058  aceq1  8499  aceq0  8500  kmlem14  8544  dfackm  8547  zfac  8841  ac6n  8866  zfcndrep  8993  zfcndac  8998  axgroth6  9207  axgroth4  9211  grothprim  9213  prime  10942  raluz2  11131  fsuppmapnn0ub  12070  mptnn0fsuppr  12074  rpnnen2  13823  isprm2  14087  isprm4  14089  pgpfac1  16945  pgpfac  16949  isirred2  17163  pmatcollpw2lem  19085  fvmptnn04if  19157  isclo2  19395  lmres  19607  ist1-2  19654  is1stc2  19749  alexsubALTlem3  20376  itg2cn  21997  ellimc3  22110  plydivex  22519  vieta1  22534  dchrelbas2  23337  ecgrtg  24059  nmobndseqi  25467  nmobndseqiOLD  25468  cvnbtwn3  26980  elat2  27032  ssrelf  27236  funcnvmptOLD  27278  resf1o  27322  isarchi2  27488  archiabl  27501  orngsqr  27554  signstfvneq0  28280  axinfprim  28829  dfon2lem9  29076  dffr4  29115  dffun10  29417  df3nandALT1  29715  df3nandALT2  29716  elicc3  29988  filnetlem4  30029  sbcalf  30347  sbcexf  30348  scott0f  30408  dford4  30802  pm10.541  31077  pm13.196a  31126  2sbc6g  31127  jcn  31236  ssfiunibd  31313  iccdifioo  31346  sumnnodd  31399  icccncfext  31453  volioc  31517  dirkercncflem2  31631  fourierdlem20  31654  fourierdlem63  31697  fourierdlem65  31699  fourierdlem81  31715  fourierdlem103  31737  fourierdlem104  31738  rmoanim  31878  ldepslinc  32408  sbidd-misc  32411  expcomdg  32565  impexpd  32579  bnj1098  33138  bnj1533  33206  bnj121  33224  bnj124  33225  bnj130  33228  bnj153  33234  bnj207  33235  bnj611  33272  bnj864  33276  bnj865  33277  bnj1000  33295  bnj978  33303  bnj1021  33318  bnj1047  33325  bnj1049  33326  bnj1090  33331  bnj1110  33334  bnj1128  33342  bnj1145  33345  bnj1171  33352  bnj1172  33353  bnj1174  33355  bnj1176  33357  bnj1280  33372  bj-alimex  33512  bj-sbnf  33710  lcvnbtwn3  34042  isat3  34321  cdleme25cv  35371  cdlemefrs29bpre0  35409  cdlemk35  35925  frege60b  37112