MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impbid2 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  euan  2295  cgsexg  2930  cgsex2g  2931  cgsex4g  2932  elab3gf  3030  abidnf  3046  elsnc2g  3785  difsn  3876  eqsn  3903  prel12  3917  dfnfc2  3975  intmin4  4021  dfiin2g  4066  elpw2g  4304  ord0eln0  4576  difex2  4654  dfwe2  4702  ordpwsuc  4735  ordunisuc2  4764  limsssuc  4770  dfom2  4787  ssrel  4904  ssrel2  4906  ssrelrel  4916  releldmb  5044  relelrnb  5045  cnveqb  5266  dmsnopg  5281  relcnvtr  5329  relcnvexb  5347  f1ocnvb  5628  ffvresb  5839  soisores  5986  fnoprabg  6110  riotaclbg  6525  dfsmo2  6545  omord  6747  nneob  6831  pw2f1olem  7148  sucdom  7240  fieq0  7361  hartogslem1  7444  rankr1ag  7661  rankeq0b  7719  fidomtri  7813  fidomtri2  7814  isfin2-2  8132  enfin2i  8134  isfin3-2  8180  isf34lem6  8193  isfin1-2  8198  isfin1-3  8199  isfin7-2  8209  axgroth6  8636  ltsonq  8779  ltexnq  8785  znegclb  10246  rpneg  10573  nltpnft  10686  ngtmnft  10687  xrrebnd  10688  qextlt  10721  qextle  10722  iccneg  10950  fzsn  11026  fz1sbc  11054  fzofzp1b  11117  hashclb  11568  hashnncl  11572  hashfun  11627  reim0b  11851  rexanre  12077  rexuzre  12083  lo1resb  12285  o1resb  12287  dvdsext  12827  pceq0  13171  pc11  13180  pcz  13181  ramtcl  13305  pospo  14357  oduposb  14490  cnvpsb  14572  tsrlemax  14579  issubg2  14886  issubg4  14888  ghmmhmb  14944  mndodcong  15107  issubrg2  15815  lpigen  16254  cyggic  16776  ip2eq  16807  eltg3  16950  bastop  16969  0top  16971  iscld3  17051  isclo2  17075  cnprest  17275  dfcon2  17403  cmphaushmeo  17753  reghaus  17778  nrmhaus  17779  fbun  17793  fsubbas  17820  ufileu  17872  uffix  17874  txflf  17959  fclsrest  17977  flimfnfcls  17981  ptcmplem2  18005  tgpt1  18068  tgpt0  18069  isngp2  18515  nrgdomn  18578  nmhmcn  18999  iscmet3  19117  limcflf  19635  ply1nzb  19912  coe11  20038  dgreq0  20050  sqf11  20789  sqff1o  20832  lgsabs1  20985  lgsquadlem2  21006  usgrafilem2  21292  cusgrafilem3  21356  elghomlem2  21798  nmobndi  22124  hmopadj2  23292  mdslle1i  23668  mdslle2i  23669  eldmgm  24585  rescon  24712  cvmsval  24732  funsseq  25149  brcolinear  25707  outsideofeu  25779  lineunray  25795  nn0prpw  26017  comppfsc  26078  cover2  26106  eqfnun  26114  isbndx  26182  isbnd2  26183  equivbnd2  26192  prdsbnd2  26195  isdrngo3  26266  ceqsex3OLD  26400  wepwsolem  26807  pmtrmvd  27067  pm11.71  27265  pm14.122b  27292  pm14.123b  27295  iotavalb  27299  climreeq  27407  rexrsb  27615  reuan  27626  afv0nbfvbi  27684  dfafn5b  27694  bnj1173  28709  lssatle  29130  opcon3b  29311  cdlemk33N  31023  cdlemk34  31024
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