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

Assertion

Ref	Expression
imbi2i

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		imbi2i.1	. . 3
2	1	a1i 11	. 2
3	2	pm5.74i 245	1

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

This theorem is referenced by:  iman  424  pm4.14  578  nan  580  pm5.32  636  anidmdbi  646  imimorb  877  pm5.6  912  nannan  1348  alimex  1652  19.36v  1762  19.36  1964  sblim  2138  sban  2140  sbhb  2182  2sb6  2188  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  moabs  2315  eu1  2327  2eu6OLD  2384  r2allem  2832  r2alfOLD  2834  r3al  2837  r19.21t  2854  r19.21tOLD  2855  r19.21v  2862  ralbii  2888  r19.35  3004  reu2  3287  reu8  3295  2reu5lem3  3307  ssconb  3636  ssin  3719  difin  3734  reldisj  3870  ssundif  3911  raldifsni  4160  pwpw0  4178  pwsnALT  4244  unissb  4281  moabex  4711  dffr2  4849  dfepfr  4869  ssrel  5096  ssrel2  5098  dffr3  5374  fncnv  5657  fun11  5658  dff13  6166  marypha2lem3  7917  dfsup2  7922  wemapsolem  7996  inf2  8061  axinf2  8078  aceq1  8519  aceq0  8520  kmlem14  8564  dfackm  8567  zfac  8861  ac6n  8886  zfcndrep  9013  zfcndac  9018  axgroth6  9227  axgroth4  9231  grothprim  9233  prime  10968  raluz2  11159  fsuppmapnn0ub  12101  mptnn0fsuppr  12105  rpnnen2  13959  isprm2  14225  isprm4  14227  pgpfac1  17131  pgpfac  17135  isirred2  17350  pmatcollpw2lem  19278  isclo2  19589  lmres  19801  ist1-2  19848  is1stc2  19943  alexsubALTlem3  20549  itg2cn  22170  ellimc3  22283  plydivex  22693  vieta1  22708  dchrelbas2  23512  nmobndseqi  25694  nmobndseqiOLD  25695  cvnbtwn3  27207  elat2  27259  ssrelf  27466  funcnvmptOLD  27509  isarchi2  27729  archiabl  27742  signstfvneq0  28529  axinfprim  29078  dfon2lem9  29223  dffr4  29262  dffun10  29564  df3nandALT1  29862  df3nandALT2  29863  elicc3  30135  filnetlem4  30199  dford4  30971  pm10.541  31272  pm13.196a  31321  2sbc6g  31322  jcn  31427  fsummulc1f  31569  dvmptmulf  31734  dvmptfprodlem  31741  rmoanim  32184  ldepslinc  33110  sbidd-misc  33113  expcomdg  33269  impexpd  33283  bnj1098  33842  bnj1533  33910  bnj121  33928  bnj124  33929  bnj130  33932  bnj153  33938  bnj207  33939  bnj611  33976  bnj864  33980  bnj865  33981  bnj1000  33999  bnj978  34007  bnj1021  34022  bnj1047  34029  bnj1049  34030  bnj1090  34035  bnj1110  34038  bnj1128  34046  bnj1145  34049  bnj1171  34056  bnj1172  34057  bnj1174  34059  bnj1176  34061  bnj1280  34076  bj-sbnf  34412  lcvnbtwn3  34753  isat3  35032  cdleme25cv  36084  cdlemefrs29bpre0  36122  cdlemk35  36638  bj-ifidg  37707  bj-ifid1g  37708  bj-ifbibib  37721  bj-ifororb  37726  elintima  37765  frege60b  37932  int-rightdistd  38001  int-sqdefd  38002  int-sqgeq0d  38007

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