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  2213  cgsexg  2832  cgsex2g  2833  cgsex4g  2834  elab3gf  2932  abidnf  2947  elsnc2g  3681  difsn  3768  eqsn  3791  prel12  3805  dfnfc2  3861  intmin4  3907  dfiin2g  3952  elpw2g  4190  ord0eln0  4462  difex2  4541  dfwe2  4589  ordpwsuc  4622  ordunisuc2  4651  limsssuc  4657  dfom2  4674  ssrel  4792  ssrelrel  4803  releldmb  4929  relelrnb  4930  cnveqb  5145  dmsnopg  5160  relcnvtr  5208  relcnvexb  5226  f1ocnvb  5502  ffvresb  5706  soisores  5840  fnoprabg  5961  riotaclbg  6360  dfsmo2  6380  omord  6582  nneob  6666  pw2f1olem  6982  sucdom  7074  fieq0  7190  hartogslem1  7273  rankr1ag  7490  rankeq0b  7548  fidomtri  7642  fidomtri2  7643  isfin2-2  7961  enfin2i  7963  isfin3-2  8009  isf34lem6  8022  isfin1-2  8027  isfin1-3  8028  isfin7-2  8038  axgroth6  8466  ltsonq  8609  ltexnq  8615  znegclb  10072  rpneg  10399  nltpnft  10511  ngtmnft  10512  xrrebnd  10513  qextlt  10546  qextle  10547  iccneg  10773  fzsn  10849  fz1sbc  10875  fzofzp1b  10933  hashclb  11368  hashnncl  11370  hashfun  11405  reim0b  11620  rexanre  11846  rexuzre  11852  lo1resb  12054  o1resb  12056  dvdsext  12595  pceq0  12939  pc11  12948  pcz  12949  ramtcl  13073  pospo  14123  oduposb  14256  cnvpsb  14338  tsrlemax  14345  issubg2  14652  issubg4  14654  ghmmhmb  14710  mndodcong  14873  issubrg2  15581  lpigen  16024  cyggic  16542  ip2eq  16573  eltg3  16716  bastop  16735  0top  16737  iscld3  16817  isclo2  16841  cnprest  17033  dfcon2  17161  cmphaushmeo  17507  reghaus  17532  nrmhaus  17533  fbun  17551  fsubbas  17578  ufileu  17630  uffix  17632  txflf  17717  fclsrest  17735  flimfnfcls  17739  ptcmplem2  17763  tgpt1  17816  tgpt0  17817  isngp2  18135  nrgdomn  18198  nmhmcn  18617  iscmet3  18735  limcflf  19247  ply1nzb  19524  coe11  19650  dgreq0  19662  sqf11  20393  sqff1o  20436  lgsabs1  20589  lgsquadlem2  20610  elghomlem2  21045  nmobndi  21369  hmopadj2  22537  mdslle1i  22913  mdslle2i  22914  eldmgm  23709  rescon  23792  cvmsval  23812  funsseq  24196  brcolinear  24754  outsideofeu  24826  lineunray  24842  dupre2  25347  svs3  25591  iepiclem  25926  isside  26269  nn0prpw  26342  comppfsc  26410  cover2  26461  eqfnun  26490  isbndx  26609  isbnd2  26610  equivbnd2  26619  prdsbnd2  26622  isdrngo3  26693  ceqsex3OLD  26829  wepwsolem  27241  pmtrmvd  27501  pm11.71  27699  pm14.122b  27726  pm14.123b  27729  iotavalb  27733  climreeq  27842  rexrsb  28050  reuan  28061  afv0nbfvbi  28119  dfafn5b  28129  cusgrauvtx  28309  bnj1173  29348  lssatle  29827  opcon3b  30008  cdlemk33N  31720  cdlemk34  31721
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