Theorem imbi1d 317

Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

Ref	Expression
imbid.1

Assertion

Ref	Expression
imbi1d

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . . 4
2	1	biimprd 223	. . 3
3	2	imim1d 75	. 2
4	1	biimpd 207	. . 3
5	4	imim1d 75	. 2
6	3, 5	impbid 191	1

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

This theorem is referenced by:  imbi12d  320  imbi1  323  imim21b  367  pm5.33  878  con3th  958  ax12vOLD  1856  19.21t  1904  ax12v2  2083  drsb1  2118  ax12inda  2278  ax12v2-o  2279  ralcom2  3022  raleqf  3050  ralxpxfr2d  3224  alexeqg  3228  alexeq  3229  mo2icl  3278  sbc19.21g  3400  csbiebg  3457  ralss  3565  r19.37zv  3925  ssuni  4271  intmin4  4316  ssexg  4598  pocl  4812  vtoclr  5049  frsn  5075  fun11  5658  funimass4  5924  dff13  6166  f1mpt  6169  isopolem  6241  oprabid  6323  caovcan  6479  caoftrn  6575  ordunisuc2  6679  tfisi  6693  tfinds  6694  tfindsg  6695  tfindsg2  6696  dfom2  6702  findsg  6727  frxp  6910  dfsmo2  7037  qliftfun  7415  ecoptocl  7420  ecopovtrn  7433  dom2lem  7575  findcard  7779  findcard2  7780  findcard3  7783  fiint  7817  supmo  7932  eqsup  7936  suplub  7940  supmaxlemOLD  7945  supisoex  7953  wemaplem1  7992  wemaplem2  7993  wemapsolem  7996  oemapvali  8124  cantnf  8133  cantnfOLD  8155  wemapwe  8160  wemapweOLD  8161  karden  8334  aceq1  8519  zorn2lem1  8897  axrepndlem2  8989  axregndlem2  9001  pwfseqlem4  9061  gruurn  9197  indpi  9306  nqereu  9328  prcdnq  9392  supexpr  9453  ltsosr  9492  supsrlem  9509  supsr  9510  axpre-lttrn  9564  axpre-sup  9567  prodgt0  10412  infm3  10527  prime  10968  raluz  11158  zsupss  11200  uzsupss  11203  xrsupsslem  11527  xrinfmsslem  11528  fz1sbc  11783  ssnn0fi  12094  brfi1uzind  12532  wrdind  12702  wrd2ind  12703  rexanre  13179  rexico  13186  limsupgle  13300  rlim2lt  13320  rlim3  13321  ello12  13339  ello12r  13340  ello1d  13346  elo12  13350  elo12r  13351  rlimconst  13367  lo1resb  13387  o1resb  13389  rlimcn2  13413  addcn2  13416  mulcn2  13418  reccn2  13419  cn1lem  13420  o1rlimmul  13441  lo1le  13474  caucvgrlem  13495  divrcnv  13664  rpnnen2  13959  sqrt2irr  13982  exprmfct  14251  isprm5  14253  prmdvdsexpr  14257  prmpwdvds  14422  vdwmc2  14497  ramtlecl  14518  ramub  14531  rami  14533  ramcl  14547  firest  14830  mreexexd  15045  acsfn  15056  prslem  15560  ispos  15576  posi  15579  isposd  15585  lubeldm  15611  lubval  15614  glbeldm  15624  glbval  15627  joinval2lem  15638  meetval2lem  15652  pospropd  15764  odlem1  16559  mndodcongi  16567  gexlem1  16599  sylow1lem3  16620  efgredlemb  16764  efgred  16766  frgpnabllem1  16877  isrrg  17936  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  ltbval  18136  opsrval  18139  xrsdsreclb  18465  islindf4  18873  mdetunilem1  19114  mdetunilem3  19116  mdetunilem4  19117  mdetunilem9  19122  chpscmat  19343  chfacffsupp  19357  chfacfscmulfsupp  19360  chfacfpmmulfsupp  19364  istopg  19404  isclo2  19589  neiptoptop  19632  neiptopnei  19633  lmbr  19759  ist0  19821  ist1-2  19848  t1sep2  19870  cmpfi  19908  2ndcdisj  19957  1stccn  19964  iskgen3  20050  ptpjopn  20113  hausdiag  20146  xkopt  20156  ist0-4  20230  isr0  20238  r0sep  20249  fbfinnfr  20342  fmfnfmlem2  20456  fmfnfmlem4  20458  fmfnfm  20459  cnflf  20503  cnfcf  20543  tmdgsum2  20595  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  tsmsxplem1  20655  tsmsxp  20657  ustssel  20708  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ust0  20722  ustuqtop4  20747  utopsnneiplem  20750  isucn2  20782  iducn  20786  metcnp  21044  metcnpi3  21049  txmetcnp  21050  metucnOLD  21091  metucn  21092  ngptgp  21150  nlmvscnlem1  21195  nrginvrcnlem  21199  nghmcn  21252  xrge0tsms  21339  xmetdcn2  21342  metdscn  21360  addcnlem  21368  elcncf1di  21399  ipcnlem1  21685  caucfil  21722  metcld  21744  metcld2  21745  volcn  22015  itg2cnlem2  22169  ellimc2  22281  dveflem  22380  dvne0  22412  mdegleb  22464  mdegle0  22477  ply1divex  22537  fta1g  22568  dgrco  22672  plydivex  22693  fta1  22704  vieta1  22708  abelthlem8  22834  divlogrlim  23016  cxpcn3lem  23121  rlimcnp  23295  cxplim  23301  cxploglim  23307  ftalem1  23346  ftalem2  23347  dvdsmulf1o  23470  ppiublem1  23477  dchrinv  23536  lgseisenlem2  23625  2sqlem6  23644  2sqlem8  23647  2sqlem10  23649  dchrisum0  23705  istrkgc  23851  istrkgb  23852  axtgcgrid  23860  axtg5seg  23862  axtgpasch  23864  axtgupdim2  23869  axtgeucl  23870  axlowdimlem15  24259  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  3v3e3cycl1  24644  constr3trllem2  24651  4cycl4v4e  24666  4cycl4dv4e  24668  eupatrl  24968  frgrawopreglem2  25045  usg2spot2nb  25065  friendshipgt3  25121  rngoidmlem  25425  isnvlem  25503  vacn  25604  nmcvcn  25605  smcnlem  25607  blocni  25720  norm3lemt  26069  isch2  26141  chlimi  26152  omlsii  26321  eigorth  26757  0cnop  26898  0cnfn  26899  idcnop  26900  lnconi  26952  stcltr1i  27193  elat2  27259  funcnv5mpt  27511  xrge0infss  27580  resspos  27647  xrge0tsmsd  27775  qqhcn  27972  qqhucn  27973  eulerpartlemgvv  28315  sgn3da  28480  sgnnbi  28484  sgnpbi  28485  erdszelem8  28642  mclsval  28923  mclsax  28929  mclsppslem  28943  ghomf1olem  29034  climuzcnv  29037  relexpindlem  29062  relexpind  29063  rtrclreclem.trans  29069  rtrclind  29072  poseq  29333  frrlem4  29390  nocvxminlem  29450  ifscgr  29694  idinside  29734  brsegle  29758  wl-sbrimt  29998  fin2so  30040  heicant  30049  mbfresfi  30061  itg2addnc  30069  ftc1anc  30098  trer  30134  filnetlem4  30199  filbcmb  30231  sdclem2  30235  fdc  30238  fdc1  30239  divrngidl  30425  pridlval  30430  smprngopr  30449  aomclem8  31007  hbtlem5  31077  acsfn1p  31148  isprm7  31192  2sbc6g  31322  sbiota1  31341  mullimc  31622  limcdm0  31624  mullimcf  31629  constlimc  31630  idlimc  31632  limsupre  31647  limcleqr  31650  addlimc  31654  0ellimcdiv  31655  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvmptfprodlem  31741  wallispilem3  31849  fourierdlem48  31937  fourierdlem87  31976  usgra2pthspth  32351  usgra2pthlem1  32353  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  aacllem  33216  bnj1145  34049  bnj1171  34056  bnj1172  34057  bj-con3thALT  34162  bj-axc15v  34330  bj-19.21t  34403  isat3  35032  iscvlat2N  35049  psubspset  35468  ldilfset  35832  ldilset  35833  dilfsetN  35877  dilsetN  35878  cdlemefrs29bpre0  36122  cdlemefrs29clN  36125  cdlemefrs32fva  36126  cdlemn11pre  36937  dihord2pre  36952  lpolsetN  37209  bj-ifbi1  37699  bj-ifbi12  37702  bj-ifbi13  37703

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