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

Theorem impbid2 207
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 206 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
43bicomd 204 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  biimt  336  biorf  406  biorfi  408  pm4.72  884  biort  904  bimsc1  946  ax13b  1857  cgsexg  3120  cgsex2g  3121  cgsex4g  3122  elab3gf  3229  abidnf  3246  elsnc2g  4032  difsn  4137  eqsn  4164  prel12  4180  dfnfc2  4240  intmin4  4288  dfiin2g  4335  elpw2g  4588  ssrel  4943  ssrel2  4945  ssrelrel  4955  releldmb  5089  relelrnb  5090  cnveqb  5311  dmsnopg  5327  relcnvtr  5375  ord0eln0  5496  f1ocnvb  5844  ffvresb  6069  soisores  6233  riotaclb  6304  fnoprabg  6411  difex2  6612  dfwe2  6622  ordpwsuc  6656  ordunisuc2  6685  limsssuc  6691  dfom2  6708  relcnvexb  6755  dfsmo2  7074  omord  7277  nneob  7361  pw2f1olem  7682  sucdom  7775  fundmfibi  7861  f1dmvrnfibi  7864  fieq0  7941  hartogslem1  8057  rankr1ag  8272  rankeq0b  8330  fidomtri  8426  fidomtri2  8427  isfin2-2  8747  enfin2i  8749  isfin3-2  8795  isf34lem6  8808  isfin1-2  8813  isfin1-3  8814  isfin7-2  8824  axgroth6  9252  ltsonq  9393  ltexnq  9399  znegclb  10974  rpneg  11332  nltpnft  11461  ngtmnft  11462  xrrebnd  11463  qextlt  11496  qextle  11497  iccneg  11751  fzsn  11838  fz1sbc  11868  fzofzp1b  12006  ceilidz  12076  fleqceilz  12078  hashclb  12537  hashnncl  12544  hashfun  12604  reim0b  13161  rexanre  13388  rexuzre  13394  lo1resb  13606  o1resb  13608  dvdsext  14334  ncoprmgcdne1b  14626  pceq0  14783  pc11  14792  pcz  14793  ramtcl  14927  ramtclOLD  14928  cshwsiun  15033  pospo  16170  oduposb  16333  cnvpsb  16410  tsrlemax  16417  issubg2  16783  issubg4  16787  ghmmhmb  16845  pmtrmvd  17048  mndodcong  17133  issubrg2  17963  lpigen  18415  cyggic  19074  ip2eq  19151  maducoeval2  19596  eltg3  19908  bastop  19928  0top  19930  iscld3  20011  isclo2  20035  cnprest  20236  dfcon2  20365  comppfsc  20478  cmphaushmeo  20746  reghaus  20771  nrmhaus  20772  fbun  20786  fsubbas  20813  ufileu  20865  uffix  20867  txflf  20952  fclsrest  20970  flimfnfcls  20974  ptcmplem2  20999  tgpt1  21063  tgpt0  21064  isngp2  21542  nrgdomn  21605  nmhmcn  22027  iscmet3  22156  limcflf  22713  ply1nzb  22948  coe11  23075  dgreq0  23087  eldmgm  23812  sqf11  23929  sqff1o  23972  lgsabs1  24125  lgsquadlem2  24146  usgrafilem2  24985  cusgrafilem3  25054  iswlkg  25097  wwlkn0s  25278  isclwlkg  25328  el2wlksoton  25451  el2spthsoton  25452  vdiscusgra  25494  elghomlem2OLD  25935  nmobndi  26261  hmopadj2  27429  mdslle1i  27805  mdslle2i  27806  relfi  28052  ssrelf  28060  bnj1173  29599  rescon  29757  cvmsval  29777  elmrsubrn  29946  funsseq  30196  brcolinear  30611  outsideofeu  30683  lineunray  30699  nn0prpw  30764  bj-19.3t  31032  bj-sb3b  31170  bj-sngltag  31326  bj-elid2  31385  bj-inftyexpiinj  31396  wl-sb5nae  31594  wl-ax11-lem2  31619  poimirlem26  31669  poimirlem27  31670  heicant  31678  cover2  31743  eqfnun  31751  isbndx  31817  isbnd2  31818  equivbnd2  31827  prdsbnd2  31830  isdrngo3  31901  ceqsex3OLD  32139  riotaclbgBAD  32234  lssatle  32289  opcon3b  32470  cdlemk33N  34184  cdlemk34  34185  wepwsolem  35605  rp-fakeimass  35854  intimag  35886  pm11.71  36383  pm14.122b  36410  pm14.123b  36413  iotavalb  36417  climreeq  37264  rexrsb  37980  reuan  37991  afv0nbfvbi  38042  dfafn5b  38052  zob  38152  zeo2ALTV  38189  elfz2z  38403  usgfislem2  38514  usgfisALTlem2  38518  nnlog2ge0lt1  39137
  Copyright terms: Public domain W3C validator