MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impbid2 Structured version   Visualization version   GIF version

Theorem impbid2 214
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
StepHypRef Expression
1 impbid2.2 . . 3 (𝜑 → (𝜒𝜓))
2 impbid2.1 . . 3 (𝜓𝜒)
31, 2impbid1 213 . 2 (𝜑 → (𝜒𝜓))
43bicomd 211 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  biimt  348  biorf  418  biorfiOLD  421  pm4.72  915  biort  935  bimsc1  975  ax13b  1949  cgsexg  3206  cgsex2g  3207  cgsex4g  3208  elab3gf  3320  abidnf  3337  elsn2g  4152  eqoreldif  4167  difsn  4264  eqsnOLD  4295  prel12  4314  elpreqprb  4326  dfnfc2  4380  dfnfc2OLD  4381  intmin4  4431  dfiin2g  4479  elpw2g  4745  ssrel  5116  ssrel2  5118  ssrelrel  5128  releldmb  5264  relelrnb  5265  cnveqb  5490  dmsnopg  5506  relcnvtr  5554  elsnxp  5576  ord0eln0  5678  f1ocnvb  6044  ffvresb  6282  isof1oopb  6449  soisores  6451  riotaclb  6522  fnoprabg  6633  difex2  6836  dfwe2  6846  ordpwsuc  6880  ordunisuc2  6909  limsssuc  6915  dfom2  6932  relcnvexb  6980  dfsmo2  7304  omord  7508  nneob  7592  pw2f1olem  7922  sucdom  8015  fundmfibi  8103  f1dmvrnfibi  8106  fieq0  8183  hartogslem1  8303  rankr1ag  8521  rankeq0b  8579  fidomtri  8675  fidomtri2  8676  isfin2-2  8997  enfin2i  8999  isfin3-2  9045  isf34lem6  9058  isfin1-2  9063  isfin1-3  9064  isfin7-2  9074  axgroth6  9502  ltsonq  9643  ltexnq  9649  znegclb  11243  rpneg  11691  nltpnft  11826  ngtmnft  11827  xrrebnd  11828  qextlt  11863  qextle  11864  iccneg  12116  fzsn  12205  fz1sbc  12236  fzofzp1b  12383  ceilidz  12464  fleqceilz  12466  hashclb  12959  hashnncl  12966  hashfun  13032  reim0b  13649  rexanre  13876  rexuzre  13882  lo1resb  14085  o1resb  14087  dvdsext  14823  zob  14863  ncoprmgcdne1b  15143  pceq0  15355  pc11  15364  pcz  15365  ramtcl  15494  cshwsiun  15586  pospo  16738  oduposb  16901  cnvpsb  16978  tsrlemax  16985  issubg2  17374  issubg4  17378  ghmmhmb  17436  pmtrmvd  17641  mndodcong  17726  issubrg2  18565  lpigen  19019  cyggic  19681  ip2eq  19758  maducoeval2  20203  eltg3  20515  bastop  20534  0top  20536  iscld3  20616  isclo2  20640  cnprest  20841  dfcon2  20970  comppfsc  21083  cmphaushmeo  21351  reghaus  21376  nrmhaus  21377  fbun  21392  fsubbas  21419  ufileu  21471  uffix  21473  txflf  21558  fclsrest  21576  flimfnfcls  21580  ptcmplem2  21605  tgpt1  21669  tgpt0  21670  isngp2  22148  nrgdomn  22214  nmhmcn  22655  iscmet3  22813  limcflf  23364  ply1nzb  23599  coe11  23726  dgreq0  23738  eldmgm  24461  sqf11  24578  sqff1o  24621  zabsle1  24734  lgsabs1  24774  lgsquadlem2  24819  usgrafilem2  25703  cusgrafilem3  25771  iswlkg  25814  wwlkn0s  25995  isclwlkg  26045  el2wlksoton  26167  el2spthsoton  26168  vdiscusgra  26210  nmobndi  26816  hmopadj2  27986  mdslle1i  28362  mdslle2i  28363  relfi  28599  ssrelf  28607  bnj1173  30126  rescon  30284  cvmsval  30304  elmrsubrn  30473  funsseq  30714  brcolinear  31138  outsideofeu  31210  lineunray  31226  nn0prpw  31290  bj-19.3t  31678  bj-sb3b  31801  bj-sngltag  31963  bj-elid2  32062  bj-inftyexpiinj  32072  wl-sb5nae  32318  wl-ax11-lem2  32341  poimirlem26  32404  poimirlem27  32405  heicant  32413  cover2  32477  eqfnun  32485  isbndx  32550  isbnd2  32551  equivbnd2  32560  prdsbnd2  32563  elghomlem2OLD  32654  isdrngo3  32727  riotaclbgBAD  33057  lssatle  33119  opcon3b  33300  cdlemk33N  35014  cdlemk34  35015  wepwsolem  36429  rp-fakeimass  36675  cnvssb  36710  intimag  36766  sscon34b  37136  ntrneiiso  37208  pm11.71  37418  pm14.122b  37445  pm14.123b  37448  iotavalb  37452  climreeq  38480  rexrsb  39618  reuan  39629  afv0nbfvbi  39681  dfafn5b  39691  zeo2ALTV  39921  elfz2z  40175  issubgr2  40494  uhgrissubgr  40497  usgrfilem  40544  uvtxnbgrb  40626  cusgrfilem3  40671  vdiscusgr  40745  wwlksn0s  41055  nnlog2ge0lt1  42156
  Copyright terms: Public domain W3C validator