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

Theorem impbid2 196
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 195 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
43bicomd 193 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  biimt  326  biorf  395  biorfi  397  pm4.72  847  biort  867  bimsc1  905  ax12b  1701  euan  2337  cgsexg  2979  cgsex2g  2980  cgsex4g  2981  elab3gf  3079  abidnf  3095  elsnc2g  3834  difsn  3925  eqsn  3952  prel12  3967  dfnfc2  4025  intmin4  4071  dfiin2g  4116  elpw2g  4355  ord0eln0  4627  difex2  4706  dfwe2  4754  ordpwsuc  4787  ordunisuc2  4816  limsssuc  4822  dfom2  4839  ssrel  4956  ssrel2  4958  ssrelrel  4968  releldmb  5096  relelrnb  5097  cnveqb  5318  dmsnopg  5333  relcnvtr  5381  relcnvexb  5399  f1ocnvb  5680  ffvresb  5892  soisores  6039  fnoprabg  6163  riotaclbg  6581  dfsmo2  6601  omord  6803  nneob  6887  pw2f1olem  7204  sucdom  7296  fieq0  7418  hartogslem1  7503  rankr1ag  7720  rankeq0b  7778  fidomtri  7872  fidomtri2  7873  isfin2-2  8191  enfin2i  8193  isfin3-2  8239  isf34lem6  8252  isfin1-2  8257  isfin1-3  8258  isfin7-2  8268  axgroth6  8695  ltsonq  8838  ltexnq  8844  znegclb  10306  rpneg  10633  nltpnft  10746  ngtmnft  10747  xrrebnd  10748  qextlt  10781  qextle  10782  iccneg  11010  fzsn  11086  fz1sbc  11116  fzofzp1b  11182  hashclb  11633  hashnncl  11637  hashfun  11692  reim0b  11916  rexanre  12142  rexuzre  12148  lo1resb  12350  o1resb  12352  dvdsext  12892  pceq0  13236  pc11  13245  pcz  13246  ramtcl  13370  pospo  14422  oduposb  14555  cnvpsb  14637  tsrlemax  14644  issubg2  14951  issubg4  14953  ghmmhmb  15009  mndodcong  15172  issubrg2  15880  lpigen  16319  cyggic  16845  ip2eq  16876  eltg3  17019  bastop  17038  0top  17040  iscld3  17120  isclo2  17144  cnprest  17345  dfcon2  17474  cmphaushmeo  17824  reghaus  17849  nrmhaus  17850  fbun  17864  fsubbas  17891  ufileu  17943  uffix  17945  txflf  18030  fclsrest  18048  flimfnfcls  18052  ptcmplem2  18076  tgpt1  18139  tgpt0  18140  isngp2  18636  nrgdomn  18699  nmhmcn  19120  iscmet3  19238  limcflf  19760  ply1nzb  20037  coe11  20163  dgreq0  20175  sqf11  20914  sqff1o  20957  lgsabs1  21110  lgsquadlem2  21131  usgrafilem2  21418  cusgrafilem3  21482  elghomlem2  21942  nmobndi  22268  hmopadj2  23436  mdslle1i  23812  mdslle2i  23813  eldmgm  24798  rescon  24925  cvmsval  24945  funsseq  25385  brcolinear  25985  outsideofeu  26057  lineunray  26073  nn0prpw  26317  comppfsc  26378  cover2  26406  eqfnun  26414  isbndx  26482  isbnd2  26483  equivbnd2  26492  prdsbnd2  26495  isdrngo3  26566  ceqsex3OLD  26700  wepwsolem  27107  pmtrmvd  27366  pm11.71  27564  pm14.122b  27591  pm14.123b  27594  iotavalb  27598  climreeq  27706  rexrsb  27914  reuan  27925  afv0nbfvbi  27982  dfafn5b  27992  elfz2z  28089  cshwsiun  28249  el2wlksoton  28298  el2spthsoton  28299  bnj1173  29308  lssatle  29750  opcon3b  29931  cdlemk33N  31643  cdlemk34  31644
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator