Theorem impbid 191

Description: Deduce an equivalence from two implications. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 190. (Revised by Wolf Lammen, 3-Nov-2012.)

Hypotheses

Ref	Expression
impbid.1
impbid.2

Assertion

Ref	Expression
impbid

Proof of Theorem impbid

Step	Hyp	Ref	Expression
1		impbid.1	. . 3
2		impbid.2	. . 3
3	1, 2	impbid21d 190	. 2
4	3	pm2.43i 47	1

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

This theorem is referenced by:  bicom1  199  impbid1  203  impcon4bid  205  pm5.74  244  imbi1d  317  pm5.501  341  2falsed  351  impbida  832  dedlem0b  953  dedlema  954  dedlemb  955  ifptru  1388  ifpfal  1389  albi  1639  exbi  1666  equequ1  1798  elequ1  1821  elequ2  1823  19.21t  1904  19.23t  1909  sbequ12  1992  cbv2h  2019  dral1  2067  dral1ALT  2068  ax12b  2086  sbequ  2117  sbft  2120  sb56  2172  exsb  2212  dral1-o  2233  eupickb  2360  eupickbi  2361  2eu2  2378  eleq2d  2527  ceqsalt  3132  ceqex  3230  mob2  3279  reu6  3288  sbciegft  3358  eqsbc3r  3389  csbiebt  3454  sseq1  3524  reupick  3781  reupick2  3783  uneqdifeq  3916  prnebg  4212  disjeq2  4426  disjeq1  4429  disjxiun  4449  disjss3  4451  reusv2lem2  4654  reusv2lem3  4655  alxfr  4665  ralxfrd  4666  copsexg  4737  copsexgOLD  4738  euotd  4753  poeq2  4809  sotric  4831  sotrieq  4832  freq2  4855  seeq1  4856  seeq2  4857  tz7.7  4909  ordtri1  4916  ordtri3  4919  ordelinel  4981  iss  5326  iotaval  5567  funeq  5612  funssres  5633  f0dom0  5774  tz6.12c  5890  fnbrfvb  5913  ssimaex  5938  fvimacnv  6002  elpreima  6007  eldmrexrnb  6038  fsn  6069  fnsnb  6090  fmptsng  6092  fmptsnd  6093  fconst2g  6125  fconst5  6128  elunirn  6163  f1ocnvfvb  6185  foeqcnvco  6203  f1eqcocnv  6204  fliftfun  6210  soisores  6223  isofr  6238  isose  6239  isopo  6242  isoso  6244  f1oiso2  6248  eusvobj2  6289  oprabid  6323  f1opw2  6528  oneqmin  6640  ordsuc  6649  ordelsuc  6655  ordsucelsuc  6657  ordunisuc2  6679  limsuc  6684  f1ovv  6771  op1steq  6842  fvn0elsuppb  6936  extmptsuppeq  6943  rntpos  6987  smoiso2  7059  seqomlem2  7135  oaord  7215  oawordex  7225  oaordex  7226  omord2  7235  om00  7243  oeord  7256  nnaord  7287  nnmord  7300  nnawordex  7305  nnaordex  7306  erexb  7355  swoord1  7359  swoord2  7360  iiner  7402  eceqoveq  7435  ralxpmap  7488  omxpenlem  7638  domtriord  7683  mapxpen  7703  mapunen  7706  ssenen  7711  nneneq  7720  onomeneq  7727  nndomo  7731  en1eqsnbi  7770  fodomfib  7820  f1opwfi  7844  fsuppunbi  7870  elfiun  7910  suplub2  7941  ordiso2  7961  ordiso  7962  oieu  7985  brwdom2  8020  brwdom3  8029  cantnflem1  8129  cantnflem1OLD  8152  cardidm  8361  carddom2  8379  pm54.43  8402  pr2ne  8404  acnen  8455  acnen2  8457  alephord  8477  alephinit  8497  dfac5  8530  infdif2  8611  fictb  8646  coflim  8662  fincssdom  8724  fin23lem25  8725  isf32lem9  8762  isf34lem4  8778  fin1a2lem11  8811  axdc3lem2  8852  ficard  8961  fpwwe2lem12  9040  fpwwe2  9042  indpi  9306  nqereq  9334  1idpr  9428  ltapr  9444  leltne  9695  ltlen  9707  ltadd2  9709  ltord1  10104  mul0or  10214  ltmul1  10417  mulge0b  10437  lt2msq  10454  nnsub  10599  nn0sub  10871  zrevaddcl  10934  zltp1le  10938  zdiv  10958  nneo  10971  zeo2  10974  zmax  11208  zbtwnre  11209  qrevaddcl  11233  xrlttri  11374  xrleltne  11380  xralrple  11433  xltneg  11445  xleadd1  11476  xlemul1  11511  supxrunb1  11540  supxrunb2  11541  ioo0  11583  iccid  11603  ico0  11604  ioc0  11605  icc0  11606  difreicc  11681  iccsplit  11682  0fz1  11734  uzsplit  11779  fzm1  11787  fzrevral  11792  ssfzo12bi  11907  elfznelfzob  11916  flge  11942  modid2  12023  ssnn0fi  12094  seqf1olem1  12146  hashen  12420  hashdom  12447  hashle00  12465  hash2prb  12517  pr2pwpr  12520  hashtpg  12523  reuccats1  12706  ccats1swrdeqbi  12723  repsdf2  12750  scshwfzeqfzo  12794  shftlem  12901  shftuz  12902  abslt  13147  absle  13148  rexico  13186  cau3lem  13187  rlim2lt  13320  rlim3  13321  o1lo1  13360  rlimdm  13374  climshft  13399  o1dif  13452  isercolllem2  13488  isercoll  13490  zsum  13540  fsum  13542  fsum00  13612  incexclem  13648  zprod  13744  fprod  13748  dvdsval2  13989  moddvds  13993  negdvdsb  14000  dvdsnegb  14001  dvdscmulr  14012  dvdsmulcr  14013  dvdssub2  14023  fzo0dvdseq  14039  bitsf1ocnv  14094  sadcaddlem  14107  bitsuz  14124  dvdsgcdb  14182  gcdeq  14190  dvdssqlem  14197  isprm2lem  14224  dvdsprime  14230  dvdsprm  14240  coprm  14241  euclemma  14249  rpexp  14261  prmdiveq  14316  odzdvds  14322  pythagtrip  14358  pc2dvds  14402  pcprmpw2  14405  pcprmpw  14406  vdwapun  14492  ramtcl2  14529  firest  14830  mrieqv2d  15036  isacs2  15050  isssc  15189  setciso  15418  posasymb  15582  pleval2  15595  pltval3  15597  lublecllem  15618  joinle  15644  meetle  15658  lubun  15753  clatleglb  15756  latdisd  15820  letsr  15857  intopsn  15882  gsumval2a  15906  frmdss2  16031  isgrpid2  16086  isgrpinv  16100  symg1bas  16421  oddvdsnn0  16568  oddvds  16571  odeq  16574  odeq1  16582  gexdvds  16604  pgpfi  16625  pgpssslw  16634  fislw  16645  sylow3lem2  16648  lsmelvalm  16671  lsmlub  16683  lsmss1b  16685  lsmss2b  16687  efgs1b  16754  cyggenod  16887  cyggexb  16901  dprdfeq0  17062  dprdfeq0OLD  17069  unitmulclb  17314  dvreq1  17342  f1rhm0to0  17389  f1rhm0to0ALT  17390  drngmul0or  17417  isabvd  17469  issrngd  17510  lssats2  17646  lspsneq0  17658  lsmelval2  17731  lvecvs0or  17754  lspsneq  17768  lspsneu  17769  lidl1el  17866  lidldvgen  17903  isnzr2  17911  0ringnnzr  17917  0ring01eqbi  17921  rrgeq0  17938  domneq0  17946  ply1coe1eq  18340  cply1coe0bi  18342  znunit  18602  psgndif  18638  ipeq0  18673  ocvsscon  18706  pjdm2  18742  obselocv  18759  islinds4  18870  mat1dimelbas  18973  cramer  19193  unitgOLD  19469  tgss3  19488  clsval2  19551  isopn3  19567  elcls3  19584  opncldf1  19585  neiint  19605  neips  19614  opnneissb  19615  opnssneib  19616  opnnei  19621  tpnei  19622  opnneiid  19627  restcld  19673  restopnb  19676  tgcn  19753  tgcnp  19754  subbascn  19755  iscnp4  19764  cnpnei  19765  cncls2  19774  cncls  19775  cnntr  19776  lmss  19799  hausnei2  19854  lpcls  19865  ordtt1  19880  cmpsub  19900  tgcmp  19901  1stcelcls  19962  locfincmp  20027  kgencn2  20058  ptpjpre1  20072  upxp  20124  txcn  20127  txlm  20149  tgqtop  20213  kqfvima  20231  isr0  20238  regr1lem2  20241  hmeoopn  20267  hmeocld  20268  ptuncnv  20308  fbunfip  20370  fgss2  20375  ufilb  20407  ufprim  20410  trufil  20411  cfinufil  20429  ufildr  20432  elfm2  20449  elfm3  20451  rnelfm  20454  fmfnfmlem4  20458  fmco  20462  flimtopon  20471  flimopn  20476  fbflim2  20478  flimrest  20484  flffbas  20496  cnpflf  20502  fclstopon  20513  fclsnei  20520  fclsbas  20522  fclsfnflim  20528  fclscmp  20531  ufilcmp  20533  isfcf  20535  fcfnei  20536  cnpfcf  20542  alexsubb  20546  alexsubALT  20551  cldsubg  20609  tgphaus  20615  tgpt0  20617  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  xbln0  20917  blssexps  20929  blssex  20930  isxms2  20951  prdsbl  20994  neibl  21004  metss  21011  met2ndc  21026  metrest  21027  metcnp3  21043  nmoeq0  21243  xrsxmet  21314  reconn  21333  iccpnfcnv  21444  fgcfil  21710  iscau4  21718  cfilres  21735  iunmbl2  21967  ismbf3d  22061  mbfaddlem  22067  i1faddlem  22100  i1fmullem  22101  ellimc3  22283  tdeglem4  22458  deg1nn0clb  22490  deg1lt0  22491  dvdsq1p  22561  plypf1  22609  0dgrb  22643  plymul0or  22677  ulmshft  22785  ulmcaulem  22789  ulmcau  22790  cosord  22919  eff1olem  22935  lognegb  22974  eflogeq  22986  logdivlt  23006  efopn  23039  cxpeq0  23059  cxpeq  23131  angpieqvd  23162  dcubic  23177  asinsinb  23228  acoscosb  23229  atantanb  23255  rlimcnp  23295  isppw  23388  isppw2  23389  vmappw  23390  isnsqf  23409  ppieq0  23450  fsumdvdsdiag  23460  dvdsppwf1o  23462  fsumfldivdiag  23466  chpeq0  23483  chteq0  23484  dchrptlem1  23539  lgsdir2lem4  23601  lgsne0  23608  lgsqr  23621  lgsdchrval  23622  lgsquadlem1  23629  m1lgs  23637  brbtwn  24202  brcgr  24203  brbtwn2  24208  axcontlem7  24273  ausisusgra  24355  nbgraf1olem5  24445  edgusgranbfin  24450  nb3graprlem1  24451  cusgrarn  24459  nbcusgra  24463  cusgrafilem2  24480  uvtxnbgra  24493  uvtxnb  24497  spthonepeq  24589  3v3e3cycl  24665  wlkiswwlk  24698  wlklniswwlkn  24701  wwlknextbi  24725  wwlknredwwlkn0  24727  wwlkextwrd  24728  wwlkextprop  24744  0clwlk  24765  clwlkisclwwlklem0  24788  el2wlkonot  24869  el2spthonot  24870  el2wlkonotot0  24872  el2wlksotot  24882  usg2wlkonot  24883  usg2spthonot  24888  usg2spthonot0  24889  nbhashuvtx  24916  uvtxhashnb  24917  0eusgraiff0rgra  24939  cusgraiffrusgra  24940  eupath2lem3  24979  frgra3vlem2  25001  frgrancvvdeqlem3  25032  numclwwlkun  25079  grpoinvf  25242  rngosn3  25428  rngoueqz  25432  rngoridfz  25437  nvmul0or  25547  nvz  25572  diporthcom  25629  ubthlem3  25788  hvmul0or  25942  his6  26016  hial0  26019  hial02  26020  orthcom  26025  normgt0  26044  ocin  26214  occon3  26215  shsel3  26233  shlub  26332  chssoc  26414  h1de2bi  26472  spansncol  26486  elspansn4  26491  spansnss2  26493  sumspansn  26567  lnopcnbd  26955  lnfncnbd  26976  riesz1  26984  elpjrn  27109  cvcon3  27203  dmdmd  27219  dmdbr3  27224  dmdbr4  27225  dmdbr5  27227  mdslmd1i  27248  atcveq0  27267  chcv1  27274  atssma  27297  atcv0eq  27298  atcv1  27299  bian1d  27366  br8d  27463  fpwrelmap  27556  xaddeq0  27573  eliccelico  27588  elicoelioo  27589  isarchiofld  27807  unitdivcld  27883  xrge0iifcnv  27915  lmxrge0  27934  indf1ofs  28039  eulerpartlemgh  28317  dstfrvunirn  28413  cvmliftmolem2  28727  cvmlift2lem12  28759  mthmb  28941  ghomf1olem  29034  climuzcnv  29037  relexpindlem  29062  br8  29185  br6  29186  br4  29187  funbreq  29201  fprb  29203  axext4dist  29233  nodenselem8  29448  dfrdg4  29600  cgrcom  29640  cgrcoml  29646  cgrdegen  29654  btwncom  29664  brsegle  29758  brsegle2  29759  colinbtwnle  29768  btwnoutside  29775  broutsideof3  29776  outsidele  29782  lineunray  29797  lineelsb2  29798  elhf2  29832  ontgval  29896  ordtop  29901  ordcmp  29912  nndivsub  29922  wl-lem-exsb  30015  wl-mo3t  30021  wl-ax11-lem1  30025  cnambfre  30063  itg2addnc  30069  elicc3  30135  nn0prpwlem  30140  opnbnd  30143  cldbnd  30144  opnregcld  30148  cldregopn  30149  fnessref  30175  refssfne  30176  neibastop2  30179  fnemeet2  30185  fnejoin2  30187  fgmin  30188  brabg2  30206  istotbnd3  30267  sstotbnd2  30270  sstotbnd  30271  sstotbnd3  30272  ssbnd  30284  ismtybnd  30303  reheibor  30335  grpoeqdivid  30343  grpokerinj  30347  1idl  30423  0rngo  30424  divrngidl  30425  igenval2  30463  ispridlc  30467  isdmn3  30471  prtlem10  30606  prter2  30622  elrfi  30626  diophrw  30692  eldioph2b  30696  diophin  30706  rexrabdioph  30727  rmxycomplete  30853  coprmdvdsb  30925  jm2.19  30935  jm2.26  30944  jm2.27  30950  limsuc2  30986  dgraa0p  31098  rngunsnply  31122  fiuneneq  31154  hashgcdlem  31157  isprm7  31192  lcmeq0  31206  lcmdvdsb  31217  nzss  31222  dvconstbi  31239  expgrowth  31240  bcc0  31245  axc11next  31313  pm14.24  31339  sbiota1  31341  iccintsng  31563  limcresiooub  31648  limclr  31661  dvnmul  31740  dvmptfprodlem  31741  fourierdlem50  31939  fourierdlem89  31978  fourierdlem91  31980  sigarcol  32081  rexsb  32173  2reu2  32192  ralbinrald  32204  rlimdmafv  32262  ralxfrd2  32303  2ffzoeq  32341  usgra2pth  32354  uhgrauhgbi  32374  uhg0v  32377  isassintop  32534  tpres  32554  uzlidlring  32735  rngciso  32790  rngcisoOLD  32802  ringciso  32841  ringcisoOLD  32865  domnmsuppn0  32962  lindslininds  33065  snlindsntor  33072  isldepslvec2  33086  sbcim2g  33309  sineq0ALT  33737  bnj145OLD  33782  bj-cbv2hv  34294  bj-dral1v  34326  bj-sbftv  34345  bj-sb56  34349  bj-equsal1t  34395  bj-19.21t  34403  bj-ceqsalt0  34449  bj-ceqsalt1  34450  bj-xpnzexb  34518  bj-finsumval0  34663  bj-lsub  34671  bj-ldiv  34674  bj-bary1  34681  lshpinN  34714  lsatcveq0  34757  lsatcv0eq  34772  lsatcv1  34773  islshpcv  34778  lkr0f  34819  lkrshp4  34833  lshpkrlem1  34835  lshpset2N  34844  lfl1dim  34846  lfl1dim2N  34847  lub0N  34914  glb0N  34918  oplecon3b  34925  cmtcomN  34974  cmtbr3N  34979  cmtbr4N  34980  cvrnbtwn2  35000  cvrnbtwn3  35001  cvrcon3b  35002  cvrnbtwn4  35004  cvrcmp  35008  atcvreq0  35039  atnle  35042  atlatle  35045  cvlexchb1  35055  cvlcvr1  35064  hlrelat2  35127  exatleN  35128  cvrval3  35137  cvrval4N  35138  cvrexch  35144  atcvr0eq  35150  lnnat  35151  atcvrj0  35152  atcvrj2b  35156  atltcvr  35159  atbtwn  35170  ps-1  35201  3at  35214  islln2a  35241  llncmp  35246  islpln2a  35272  lplncmp  35286  islvol2aN  35316  4at  35337  lvolcmp  35341  pmaple  35485  lncmp  35507  paddss  35569  llnexchb2lem  35592  2polcon4bN  35642  ispsubcl2N  35671  lhpat3  35770  lautcvr  35816  ltrnid  35859  trlval2  35888  trlatn0  35897  ltrnideq  35900  trlnidatb  35902  cdlemeg49lebilem  36265  trlord  36295  cdlemg1a  36296  cdlemg1cex  36314  tendoid0  36551  dva1dim  36711  cdlemm10N  36845  diarnN  36856  cdlemn  36939  dihlspsnssN  37059  dihatexv  37065  dochkrshp  37113  dochkrshp4  37116  djhlsmcl  37141  lcfl6  37227  lcfl8  37229  lcfrvalsnN  37268  lcfrlem9  37277  mapdval2N  37357  mapdordlem2  37364  mapd1o  37375  mapd0  37392  mapdheq2biN  37457  pwelg  37745

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