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

Theorem impbid2 204
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 203 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
43bicomd 201 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  biimt  335  biorf  405  biorfi  407  pm4.72  864  biort  884  bimsc1  922  ax13b  1742  euanOLD  2329  cgsexg  2994  cgsex2g  2995  cgsex4g  2996  elab3gf  3100  abidnf  3117  elsnc2g  3895  difsn  3996  eqsn  4022  prel12  4037  dfnfc2  4097  intmin4  4145  dfiin2g  4191  elpw2g  4443  ord0eln0  4760  ssrel  4915  ssrel2  4917  ssrelrel  4927  releldmb  5061  relelrnb  5062  cnveqb  5281  dmsnopg  5298  relcnvtr  5345  f1ocnvb  5642  ffvresb  5861  soisores  6005  riotaclb  6079  fnoprabg  6180  difex2  6372  dfwe2  6382  ordpwsuc  6415  ordunisuc2  6444  limsssuc  6450  dfom2  6467  relcnvexb  6515  dfsmo2  6794  omord  6995  nneob  7079  pw2f1olem  7403  sucdom  7496  fieq0  7659  hartogslem1  7744  rankr1ag  7997  rankeq0b  8055  fidomtri  8151  fidomtri2  8152  isfin2-2  8476  enfin2i  8478  isfin3-2  8524  isf34lem6  8537  isfin1-2  8542  isfin1-3  8543  isfin7-2  8553  axgroth6  8982  ltsonq  9125  ltexnq  9131  znegclb  10669  rpneg  11007  nltpnft  11125  ngtmnft  11126  xrrebnd  11127  qextlt  11160  qextle  11161  iccneg  11392  fzsn  11486  fz1sbc  11519  fzofzp1b  11608  ceilidz  11674  fleqceilz  11676  hashclb  12111  hashnncl  12117  hashfun  12182  wrdlenfi  12241  reim0b  12591  rexanre  12817  rexuzre  12823  lo1resb  13025  o1resb  13027  dvdsext  13566  pceq0  13919  pc11  13928  pcz  13929  ramtcl  14053  cshwsiun  14108  pospo  15125  oduposb  15288  cnvpsb  15365  tsrlemax  15372  issubg2  15675  issubg4  15679  ghmmhmb  15737  pmtrmvd  15941  mndodcong  16024  issubrg2  16808  lpigen  17259  cyggic  17846  ip2eq  17923  maducoeval2  18287  eltg3  18408  bastop  18427  0top  18429  iscld3  18509  isclo2  18533  cnprest  18734  dfcon2  18864  cmphaushmeo  19214  reghaus  19239  nrmhaus  19240  fbun  19254  fsubbas  19281  ufileu  19333  uffix  19335  txflf  19420  fclsrest  19438  flimfnfcls  19442  ptcmplem2  19466  tgpt1  19529  tgpt0  19530  isngp2  20030  nrgdomn  20093  nmhmcn  20516  iscmet3  20645  limcflf  21197  ply1nzb  21478  coe11  21604  dgreq0  21616  sqf11  22361  sqff1o  22404  lgsabs1  22557  lgsquadlem2  22578  usgrafilem2  23147  cusgrafilem3  23211  elghomlem2  23671  nmobndi  23997  hmopadj2  25167  mdslle1i  25543  mdslle2i  25544  ssrelf  25768  eldmgm  26855  rescon  26982  cvmsval  27002  funsseq  27426  brcolinear  27936  outsideofeu  28008  lineunray  28024  wl-sb5nae  28229  wl-ax11-lem2  28243  heicant  28267  nn0prpw  28359  comppfsc  28420  cover2  28448  eqfnun  28456  isbndx  28522  isbnd2  28523  equivbnd2  28532  prdsbnd2  28535  isdrngo3  28606  ceqsex3OLD  28847  wepwsolem  29236  pm11.71  29492  pm14.122b  29519  pm14.123b  29522  iotavalb  29526  climreeq  29629  rexrsb  29836  reuan  29847  afv0nbfvbi  29900  dfafn5b  29910  elfz2z  30041  iswlkg  30128  wwlkn0s  30182  el2wlksoton  30240  el2spthsoton  30241  isclwlkg  30263  vdiscusgra  30380  bnj1173  31692  bj-sb3b  31943  bj-sngltag  32056  bj-inftyexpiinj  32109  riotaclbgBAD  32175  riotaclbBAD  32176  lssatle  32230  opcon3b  32411  cdlemk33N  34123  cdlemk34  34124
  Copyright terms: Public domain W3C validator