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

Theorem impbid2 195
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 194 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
43bicomd 192 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  biimt  325  biorf  394  biorfi  396  pm4.72  846  biort  866  bimsc1  904  euan  2200  cgsexg  2819  cgsex2g  2820  cgsex4g  2821  elab3gf  2919  abidnf  2934  elsnc2g  3668  difsn  3755  eqsn  3775  prel12  3789  dfnfc2  3845  intmin4  3891  dfiin2g  3936  elpw2g  4174  ord0eln0  4446  difex2  4525  dfwe2  4573  ordpwsuc  4606  ordunisuc2  4635  limsssuc  4641  dfom2  4658  ssrel  4776  ssrelrel  4787  releldmb  4913  relelrnb  4914  cnveqb  5129  dmsnopg  5144  relcnvtr  5192  relcnvexb  5210  f1ocnvb  5486  ffvresb  5690  soisores  5824  fnoprabg  5945  riotaclbg  6344  dfsmo2  6364  omord  6566  nneob  6650  pw2f1olem  6966  sucdom  7058  fieq0  7174  hartogslem1  7257  rankr1ag  7474  rankeq0b  7532  fidomtri  7626  fidomtri2  7627  isfin2-2  7945  enfin2i  7947  isfin3-2  7993  isf34lem6  8006  isfin1-2  8011  isfin1-3  8012  isfin7-2  8022  axgroth6  8450  ltsonq  8593  ltexnq  8599  znegclb  10056  rpneg  10383  nltpnft  10495  ngtmnft  10496  xrrebnd  10497  qextlt  10530  qextle  10531  iccneg  10757  fzsn  10833  fz1sbc  10859  fzofzp1b  10917  hashclb  11352  hashnncl  11354  hashfun  11389  reim0b  11604  rexanre  11830  rexuzre  11836  lo1resb  12038  o1resb  12040  dvdsext  12579  pceq0  12923  pc11  12932  pcz  12933  ramtcl  13057  pospo  14107  oduposb  14240  cnvpsb  14322  tsrlemax  14329  issubg2  14636  issubg4  14638  ghmmhmb  14694  mndodcong  14857  issubrg2  15565  lpigen  16008  cyggic  16526  ip2eq  16557  eltg3  16700  bastop  16719  0top  16721  iscld3  16801  isclo2  16825  cnprest  17017  dfcon2  17145  cmphaushmeo  17491  reghaus  17516  nrmhaus  17517  fbun  17535  fsubbas  17562  ufileu  17614  uffix  17616  txflf  17701  fclsrest  17719  flimfnfcls  17723  ptcmplem2  17747  tgpt1  17800  tgpt0  17801  isngp2  18119  nrgdomn  18182  nmhmcn  18601  iscmet3  18719  limcflf  19231  ply1nzb  19508  coe11  19634  dgreq0  19646  sqf11  20377  sqff1o  20420  lgsabs1  20573  lgsquadlem2  20594  elghomlem2  21029  nmobndi  21353  hmopadj2  22521  mdslle1i  22897  mdslle2i  22898  eldmgm  23694  rescon  23777  cvmsval  23797  funsseq  24125  brcolinear  24682  outsideofeu  24754  lineunray  24770  dupre2  25244  svs3  25488  iepiclem  25823  isside  26166  nn0prpw  26239  comppfsc  26307  cover2  26358  eqfnun  26387  isbndx  26506  isbnd2  26507  equivbnd2  26516  prdsbnd2  26519  isdrngo3  26590  ceqsex3OLD  26726  wepwsolem  27138  pmtrmvd  27398  pm11.71  27596  pm14.122b  27623  pm14.123b  27626  iotavalb  27630  climreeq  27739  rexrsb  27947  reuan  27958  afv0nbfvbi  28014  dfafn5b  28023  cusgrauvtx  28168  bnj1173  29032  lssatle  29205  opcon3b  29386  cdlemk33N  31098  cdlemk34  31099
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 177
  Copyright terms: Public domain W3C validator