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

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  |-  ( ps 
->  ch )
impbid2.2  |-  ( ph  ->  ( ch  ->  ps ) )
Assertion
Ref Expression
impbid2  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbid2
StepHypRef Expression
1 impbid2.2 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
2 impbid2.1 . . 3  |-  ( ps 
->  ch )
31, 2impbid1 203 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
43bicomd 201 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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
This theorem is referenced by:  biimt  335  biorf  405  biorfi  407  pm4.72  874  biort  894  bimsc1  936  ax13b  1754  euanOLD  2354  cgsexg  3146  cgsex2g  3147  cgsex4g  3148  elab3gf  3255  abidnf  3272  elsnc2g  4057  difsn  4161  eqsn  4188  prel12  4203  dfnfc2  4263  intmin4  4311  dfiin2g  4358  elpw2g  4610  ord0eln0  4932  ssrel  5091  ssrel2  5093  ssrelrel  5103  releldmb  5237  relelrnb  5238  cnveqb  5462  dmsnopg  5479  relcnvtr  5527  f1ocnvb  5829  ffvresb  6052  soisores  6211  riotaclb  6283  fnoprabg  6387  difex2  6591  dfwe2  6601  ordpwsuc  6634  ordunisuc2  6663  limsssuc  6669  dfom2  6686  relcnvexb  6732  dfsmo2  7018  omord  7217  nneob  7301  pw2f1olem  7621  sucdom  7715  fieq0  7881  hartogslem1  7967  rankr1ag  8220  rankeq0b  8278  fidomtri  8374  fidomtri2  8375  isfin2-2  8699  enfin2i  8701  isfin3-2  8747  isf34lem6  8760  isfin1-2  8765  isfin1-3  8766  isfin7-2  8776  axgroth6  9206  ltsonq  9347  ltexnq  9353  znegclb  10900  rpneg  11249  nltpnft  11367  ngtmnft  11368  xrrebnd  11369  qextlt  11402  qextle  11403  iccneg  11641  fzsn  11725  fz1sbc  11754  fzofzp1b  11878  ceilidz  11947  fleqceilz  11949  hashclb  12398  hashnncl  12404  hashfun  12461  reim0b  12915  rexanre  13142  rexuzre  13148  lo1resb  13350  o1resb  13352  dvdsext  13896  pceq0  14253  pc11  14262  pcz  14263  ramtcl  14387  cshwsiun  14442  pospo  15460  oduposb  15623  cnvpsb  15700  tsrlemax  15707  issubg2  16021  issubg4  16025  ghmmhmb  16083  pmtrmvd  16287  mndodcong  16372  issubrg2  17249  lpigen  17703  cyggic  18406  ip2eq  18483  maducoeval2  18937  eltg3  19258  bastop  19277  0top  19279  iscld3  19359  isclo2  19383  cnprest  19584  dfcon2  19714  cmphaushmeo  20064  reghaus  20089  nrmhaus  20090  fbun  20104  fsubbas  20131  ufileu  20183  uffix  20185  txflf  20270  fclsrest  20288  flimfnfcls  20292  ptcmplem2  20316  tgpt1  20379  tgpt0  20380  isngp2  20880  nrgdomn  20943  nmhmcn  21366  iscmet3  21495  limcflf  22048  ply1nzb  22286  coe11  22412  dgreq0  22424  sqf11  23169  sqff1o  23212  lgsabs1  23365  lgsquadlem2  23386  usgrafilem2  24116  cusgrafilem3  24185  iswlkg  24228  wwlkn0s  24409  isclwlkg  24459  el2wlksoton  24582  el2spthsoton  24583  vdiscusgra  24625  elghomlem2  25068  nmobndi  25394  hmopadj2  26564  mdslle1i  26940  mdslle2i  26941  ssrelf  27167  eldmgm  28232  rescon  28359  cvmsval  28379  funsseq  28804  brcolinear  29314  outsideofeu  29386  lineunray  29402  wl-sb5nae  29612  wl-ax11-lem2  29631  heicant  29654  nn0prpw  29746  comppfsc  29807  cover2  29835  eqfnun  29843  isbndx  29909  isbnd2  29910  equivbnd2  29919  prdsbnd2  29922  isdrngo3  29993  ceqsex3OLD  30233  wepwsolem  30619  pm11.71  30909  pm14.122b  30936  pm14.123b  30939  iotavalb  30943  climreeq  31183  rexrsb  31669  reuan  31680  afv0nbfvbi  31731  dfafn5b  31741  fundmfibi  31806  f1dmvrnfibi  31807  elfz2z  31826  usgfislem2  31940  usgfisALTlem2  31944  bnj1173  33155  bj-19.3t  33352  bj-sb3b  33489  bj-sngltag  33640  bj-elid2  33691  bj-inftyexpiinj  33702  riotaclbgBAD  33775  riotaclbBAD  33776  lssatle  33830  opcon3b  34011  cdlemk33N  35723  cdlemk34  35724
  Copyright terms: Public domain W3C validator