Theorem impbida 832

Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)

Hypotheses

Ref	Expression
impbida.1
impbida.2

Assertion

Ref	Expression
impbida

Proof of Theorem impbida

Step	Hyp	Ref	Expression
1		impbida.1	. . 3
2	1	ex 434	. 2
3		impbida.2	. . 3
4	3	ex 434	. 2
5	2, 4	impbid 191	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  eqrdav  2455  eqrdavOLD  2456  frsn  5075  funfvbrb  6000  iinpreima  6017  fnprb  6129  fnprOLD  6130  nvocnv  6187  f1ocnv2d  6526  el2xptp0  6844  1stconst  6888  2ndconst  6889  cnvf1o  6899  tfrlem15  7080  oeeui  7270  ersymb  7344  swoer  7358  erth  7375  boxriin  7531  boxcutc  7532  domunsncan  7637  pw2f1olem  7641  enen1  7677  enen2  7678  domen1  7679  domen2  7680  sdomen1  7681  sdomen2  7682  xpmapenlem  7704  ordiso2  7961  wdomen1  8023  wdomen2  8024  fin23lem26  8726  fpwwe2lem8  9036  r1wunlim  9136  ixxun  11574  xov1plusxeqvd  11695  fzsplit2  11739  fseq1p1m1  11781  elfz2nn0  11798  flflp1  11944  modsubdir  12055  zesq  12289  hashprg  12460  hashgt0elexb  12467  hashbclem  12501  rereb  12953  rlimclim  13369  iserex  13479  caucvgb  13502  mptfzshft  13593  fsumrev  13594  climcnds  13663  fprodrev  13781  dvdsadd2b  14028  bitsfzo  14085  dvdsmulgcd  14192  qden1elz  14290  mrcidb  15012  mrieqvlemd  15026  isacs2  15050  ssclem  15188  issubc3  15218  ffthiso  15298  fuciso  15344  setcmon  15414  setcepi  15415  setcinv  15417  catciso  15434  acsfiindd  15807  issubmnd  15948  mhmf1o  15976  subsubm  15988  resmhm2b  15992  grpinvid1  16098  grpinvid2  16099  subsubg  16224  ssnmz  16243  ghmf1  16295  ghmf1o  16296  conjnmzb  16301  subggim  16314  gicsubgen  16326  gass  16339  odf1  16584  gex1  16611  fislw  16645  sylow3lem2  16648  sylow3lem6  16652  lsmdisj2a  16705  lsmdisj2b  16706  efgred2  16771  dmdprdsplit  17096  0unit  17329  irrednegb  17360  rhmf1o  17381  kerf1hrm  17392  isdrng2  17406  subrgunit  17447  issubdrg  17454  subsubrg  17455  islss3  17605  islss4  17608  lspsnel6  17640  lspsneq0b  17659  islmhm2  17684  lmhmf1o  17692  reslmhm2b  17700  lssvs0or  17756  lvecinv  17759  lspsnel4  17770  lspdisjb  17772  islbs2  17800  islbs3  17801  issubassa  17973  issubassa2  17994  gsumbagdiag  18028  subrgasclcl  18164  prmirredlem  18523  prmirredlemOLD  18526  islindf3  18861  lindsmm  18863  lsslindf  18865  lsslinds  18866  matunit  19180  slesolinvbi  19183  en2top  19487  elcls  19574  neindisj2  19624  neiptopnei  19633  neiptopreu  19634  maxlp  19648  neitr  19681  iscncl  19770  cncnp  19781  isreg2  19878  dis2ndc  19961  1stccnp  19963  islly2  19985  dislly  19998  dissnlocfin  20030  kgencmp2  20047  pt1hmeo  20307  xkocnv  20315  t0kq  20319  uffixfr  20424  flimcf  20483  cnpflf2  20501  fclscf  20526  cnextf  20566  utopsnneiplem  20750  isucn2  20782  cfilucfilOLD  21072  cfilucfil  21073  metutopOLD  21085  psmetutop  21086  restmetu  21090  tngngp2  21166  tngngp  21168  nmoleub  21238  metdseq0  21358  cnheibor  21455  pcophtb  21529  nmoleub2lem  21597  lmmbr  21697  iscfil3  21712  cmetss  21753  cldcss  21856  mbfeqalem  22049  mbfposb  22060  itg2const2  22148  itgss3  22221  plyco0  22589  dgrlt  22663  ulm2  22780  coseq00topi  22895  coseq0negpitopi  22896  sineq0  22914  atans2  23262  xrlimcnp  23298  dchrelbas2  23512  dchrn0  23525  2sqb  23653  istrkg2ld  23858  tgcgreqb  23872  tgbtwncomb  23880  trgcgrg  23906  legov  23972  legov2  23973  legov3  23984  hlbtwn  23995  tglineelsb2  24012  tglinecom  24015  colline  24030  mirinv  24047  mirbtwnb  24052  mirbtwnhl  24060  perpcom  24090  isperp2  24092  oppcom  24116  opphllem3  24121  lnopp2hpgb  24132  lmieu  24150  nb3graprlem1  24451  eleclclwwlknlem2  24818  clwwlknscsh  24819  el2spthonot0  24871  numclwwlk2lem1  25102  grpoinvid1  25232  grpoinvid2  25233  ismndo1  25346  leopmul  27053  hst1h  27146  disjabrex  27443  disjabrexf  27444  erbr3b  27468  f1o3d  27471  funimass4f  27474  fgreu  27513  fcnvgreu  27514  fcobij  27548  resf1o  27553  mul2lt0bi  27569  fzsplit3  27599  eliccioo  27627  ogrpinv0le  27706  ogrpaddltbi  27709  ogrpaddltrbid  27711  ogrpinv0lt  27713  isarchi3  27731  fimaproj  27836  qtophaus  27839  reff  27842  locfinreflem  27843  cmpcref  27853  metider  27873  pstmfval  27875  qqhval2  27963  aean  28216  imambfm  28233  eulerpartlemgvv  28315  orvcgteel  28406  orvclteel  28411  ballotlemsf1o  28452  sgn3da  28480  sgnnbi  28484  sgnpbi  28485  sgnmulsgn  28488  sgnmulsgp  28489  sconpi1  28684  brofs2  29727  brifs2  29728  broutsideof2  29772  ltflcei  30043  ismblfin  30055  cnambfre  30063  ftc1anclem6  30095  isdrngo2  30361  mrefg2  30639  mzpmfp  30679  mzpmfpOLD  30680  lzenom  30703  elpell14qr2  30798  elpell1qr2  30808  pellfund14b  30835  congabseq  30912  acongeq  30921  jm2.23  30938  jm2.20nn  30939  jm2.25lem1  30940  wepwsolem  30987  islssfg2  31017  lnmlmic  31034  dfacbasgrp  31057  lcmgcdeq  31216  rfcnpre3  31408  rfcnpre4  31409  ioossioobi  31557  iccshift  31558  iocopn  31560  eliccelioc  31561  iooshift  31562  icoopn  31565  limcdm0  31624  islptre  31625  islpcn  31645  limcresioolb  31649  fperdvper  31715  itgperiod  31780  fourierdlem32  31921  fourierdlem33  31922  fourierdlem48  31937  fourierdlem49  31938  fourierdlem71  31960  fourierdlem81  31970  mgmhmf1o  32475  issubmgm2  32478  subsubmgm  32485  resmgmhm2b  32488  cicer  32590  rnghmf1o  32709  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  lshpnelb  34709  lshpnel2N  34710  lsatspn0  34725  lsatelbN  34731  lsat0cv  34758  lcvexch  34764  lcv1  34766  lkrshp3  34831  lkrpssN  34888  lkrss2N  34894  cvlsupr2  35068  atcvrlln  35244  llncvrlpln  35282  2llnmj  35284  lplncvrlvol  35340  2lplnmj  35346  polcon2bN  35644  pcl0bN  35647  lhpmcvr3  35749  lhpmatb  35755  ltrncoidN  35852  ltrneq3  35933  ltrniotavalbN  36310  cdlemg1cN  36313  diclspsn  36921  dihopelvalcpre  36975  dihord4  36985  dihord  36991  dihmeetlem4preN  37033  dih1dimatlem0  37055  dochsscl  37095  dochoccl  37096  dochord  37097  dochsat  37110  dochshpncl  37111  dochsatshpb  37179  dochshpsat  37181  mapdval4N  37359  mapdsn  37368  hdmap14lem12  37609  hdmapip0  37645  hlhillcs  37688

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  df-an 371