Theorem impbid1 203

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

Hypotheses

Ref	Expression
impbid1.1
impbid1.2

Assertion

Ref	Expression
impbid1

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2
2		impbid1.2	. . 3
3	2	a1i 11	. 2
4	1, 3	impbid 191	1

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

This theorem is referenced by:  impbid2  204  iba  503  ibar  504  pm5.71  936  cad0  1467  19.33b  1696  19.40b  1698  19.9t  1890  ax16gb  1942  equs5  2092  sb4b  2098  2eu1  2376  2eu1OLD  2377  2eu3  2379  ceqsalgALT  3135  csbprc  3821  undif4  3883  sneqbg  4200  opthpr  4208  elpwuni  4418  eusv2i  4649  reusv2lem3  4655  reusv3  4660  reuxfr2d  4675  ordssun  4982  suc11  4986  unizlim  4999  soltmin  5411  ssxpb  5446  xp11  5447  xpcan  5448  xpcan2  5449  iotanul  5571  imadif  5668  2elresin  5697  mpteqb  5970  f1fveq  6170  f1elima  6171  f1imass  6172  fliftf  6213  sorpssuni  6589  sorpssint  6590  iunpw  6614  ssonprc  6627  onint0  6631  oa00  7227  omcan  7237  omopth2  7252  oecan  7257  nnarcl  7284  iserd  7356  ecopover  7434  map0g  7478  fundmen  7609  fopwdom  7645  onfin  7728  fineqvlem  7754  f1finf1o  7766  isfiniteg  7800  inficl  7905  tc00  8200  cardnueq0  8366  cardsdomel  8376  wdomfil  8463  wdomnumr  8466  alephsucdom  8481  cardalephex  8492  dfac12lem2  8545  cfeq0  8657  fin23lem24  8723  fin1a2lem9  8809  carden  8947  axrepnd  8990  axacndlem4  9009  gchpwdom  9069  gchina  9098  r1tskina  9181  addcanpi  9298  mulcanpi  9299  elnpi  9387  addcan  9785  addcan2  9786  neg11  9893  negreb  9907  add20  10089  mulcand  10207  cru  10553  nn0lt10b  10950  uz11  11132  eqreznegel  11196  lbzbi  11199  rpnnen1  11242  xrmaxlt  11411  xrltmin  11412  xrmaxle  11413  xrlemin  11414  xneg11  11443  xsubge0  11482  xrub  11532  elioc2  11616  elico2  11617  elicc2  11618  fzopth  11749  2ffzeq  11823  flidz  11947  expeq0  12196  sq01  12288  fz1eqb  12426  hashen1  12439  hash1snb  12479  wrdnval  12571  eqwrd  12582  wrdl1s1  12622  ccatopth  12695  ccatopth2  12696  wrdlen2  12886  cj11  12995  sqrt0  13075  abs00  13122  recan  13169  rlimdm  13374  rpnnen2  13959  0dvds  14004  dvds1  14034  alzdvds  14036  gcdeq0  14159  algcvgblem  14206  prmexpb  14258  prmreclem3  14436  4sqlem11  14473  moni  15131  grprcan  16083  grplcan  16102  grpinv11  16107  galcan  16342  sylow2a  16639  subgdisjb  16711  drngmuleq0  17419  lspsncmp  17762  fidomndrng  17956  coe1tm  18314  xrsdsreclb  18465  znidomb  18600  lmisfree  18877  istps2OLD  19422  tgdom  19480  en1top  19486  cmpfi  19908  txcmpb  20145  hmeocnvb  20275  flimcls  20486  hauspwpwf1  20488  flftg  20497  ghmcnp  20613  metrest  21027  icoopnst  21439  iocopnst  21440  ishl2  21810  vitali  22022  mbfi1fseqlem4  22125  aannenlem1  22724  perfect  23506  usgra1v  24390  is2wlk  24567  usgra2wlkspth  24621  usg2wotspth  24884  usg2spot2nb  25065  extwwlkfab  25090  grporcan  25223  grpolcan  25235  ip2eqi  25772  hial2eq  26023  eigorthi  26756  stge1i  27157  stle0i  27158  mdbr3  27216  mdbr4  27217  atsseq  27266  mdsymlem7  27328  eqvincg  27374  reuxfr3d  27388  disjunsn  27453  fpwrelmapffslem  27555  xmulcand  27617  prsdm  27896  prsrn  27897  mthmpps  28942  untangtr  29086  sltval2  29416  ordtopcon  29904  ordtopt0  29907  wl-lem-moexsb  30017  filnetlem4  30199  seqpo  30240  fphpd  30750  pellexlem3  30767  qirropth  30844  expdioph  30965  rpnnen3  30974  iotasbc  31326  2reu1  32191  2reu3  32193  rlimdmafv  32262  fzoopth  32340  2ffzoeq  32341  usgra2pthspth  32351  0ringdif  32676  islinindfis  33050  lincresunit3lem3  33075  bj-dfbi6  34156  bj-19.9htbi  34257  bj-ax16gb  34325  bj-equs5v  34332  bj-sb4bv  34338  lshpcmp  34713  lsatcmp  34728  lsatcmp2  34729  ltrneq2  35872  ltrneq  35873  tendospcanN  36750  dochlkr  37112  lcfl7N  37228  hgmap11  37632

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