Theorem impbid2 204

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)

Hypotheses

Ref	Expression
impbid2.1
impbid2.2

Assertion

Ref	Expression
impbid2

Proof of Theorem impbid2

Step	Hyp	Ref	Expression
1		impbid2.2	. . 3
2		impbid2.1	. . 3
3	1, 2	impbid1 203	. 2
4	3	bicomd 201	1

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

This theorem is referenced by:  biimt  335  biorf  405  biorfi  407  pm4.72  876  biort  896  bimsc1  938  ax13b  1805  cgsexg  3142  cgsex2g  3143  cgsex4g  3144  elab3gf  3251  abidnf  3268  elsnc2g  4059  difsn  4164  eqsn  4191  prel12  4207  dfnfc2  4267  intmin4  4316  dfiin2g  4363  elpw2g  4615  ord0eln0  4937  ssrel  5096  ssrel2  5098  ssrelrel  5108  releldmb  5242  relelrnb  5243  cnveqb  5467  dmsnopg  5484  relcnvtr  5532  f1ocnvb  5834  ffvresb  6062  soisores  6223  riotaclb  6295  fnoprabg  6403  difex2  6607  dfwe2  6617  ordpwsuc  6650  ordunisuc2  6679  limsssuc  6685  dfom2  6702  relcnvexb  6748  dfsmo2  7037  omord  7236  nneob  7320  pw2f1olem  7641  sucdom  7735  fieq0  7901  hartogslem1  7988  rankr1ag  8241  rankeq0b  8299  fidomtri  8395  fidomtri2  8396  isfin2-2  8720  enfin2i  8722  isfin3-2  8768  isf34lem6  8781  isfin1-2  8786  isfin1-3  8787  isfin7-2  8797  axgroth6  9227  ltsonq  9368  ltexnq  9374  znegclb  10926  rpneg  11278  nltpnft  11396  ngtmnft  11397  xrrebnd  11398  qextlt  11431  qextle  11432  iccneg  11670  fzsn  11754  fz1sbc  11783  fzofzp1b  11910  ceilidz  11979  fleqceilz  11981  hashclb  12430  hashnncl  12436  hashfun  12495  reim0b  12952  rexanre  13179  rexuzre  13185  lo1resb  13387  o1resb  13389  dvdsext  14037  pceq0  14394  pc11  14403  pcz  14404  ramtcl  14528  cshwsiun  14584  pospo  15603  oduposb  15766  cnvpsb  15843  tsrlemax  15850  issubg2  16216  issubg4  16220  ghmmhmb  16278  pmtrmvd  16481  mndodcong  16566  issubrg2  17449  lpigen  17904  cyggic  18611  ip2eq  18688  maducoeval2  19142  eltg3  19463  bastop  19483  0top  19485  iscld3  19565  isclo2  19589  cnprest  19790  dfcon2  19920  comppfsc  20033  cmphaushmeo  20301  reghaus  20326  nrmhaus  20327  fbun  20341  fsubbas  20368  ufileu  20420  uffix  20422  txflf  20507  fclsrest  20525  flimfnfcls  20529  ptcmplem2  20553  tgpt1  20616  tgpt0  20617  isngp2  21117  nrgdomn  21180  nmhmcn  21603  iscmet3  21732  limcflf  22285  ply1nzb  22523  coe11  22650  dgreq0  22662  sqf11  23413  sqff1o  23456  lgsabs1  23609  lgsquadlem2  23630  usgrafilem2  24412  cusgrafilem3  24481  iswlkg  24524  wwlkn0s  24705  isclwlkg  24755  el2wlksoton  24878  el2spthsoton  24879  vdiscusgra  24921  elghomlem2OLD  25364  nmobndi  25690  hmopadj2  26860  mdslle1i  27236  mdslle2i  27237  relfi  27459  ssrelf  27466  eldmgm  28564  rescon  28691  cvmsval  28711  elmrsubrn  28880  funsseq  29199  brcolinear  29709  outsideofeu  29781  lineunray  29797  wl-sb5nae  30007  wl-ax11-lem2  30026  heicant  30049  nn0prpw  30141  cover2  30204  eqfnun  30212  isbndx  30278  isbnd2  30279  equivbnd2  30288  prdsbnd2  30291  isdrngo3  30362  ceqsex3OLD  30601  wepwsolem  30987  pm11.71  31303  pm14.122b  31330  pm14.123b  31333  iotavalb  31337  climreeq  31619  rexrsb  32174  reuan  32185  afv0nbfvbi  32236  dfafn5b  32246  fundmfibi  32311  f1dmvrnfibi  32312  elfz2z  32331  usgfislem2  32445  usgfisALTlem2  32449  bnj1173  34058  bj-19.3t  34252  bj-sb3b  34390  bj-sngltag  34541  bj-elid2  34600  bj-inftyexpiinj  34612  riotaclbgBAD  34685  lssatle  34740  opcon3b  34921  cdlemk33N  36635  cdlemk34  36636  rp-fakeimass  37736  intimag  37770

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