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  333  biorf  403  biorfi  405  pm4.72  874  biort  894  bimsc1  936  ax13b  1810  cgsexg  3139  cgsex2g  3140  cgsex4g  3141  elab3gf  3248  abidnf  3265  elsnc2g  4046  difsn  4150  eqsn  4177  prel12  4193  dfnfc2  4253  intmin4  4301  dfiin2g  4348  elpw2g  4600  ord0eln0  4921  ssrel  5079  ssrel2  5081  ssrelrel  5091  releldmb  5226  relelrnb  5227  cnveqb  5446  dmsnopg  5462  relcnvtr  5510  f1ocnvb  5811  ffvresb  6038  soisores  6198  riotaclb  6269  fnoprabg  6376  difex2  6580  dfwe2  6590  ordpwsuc  6623  ordunisuc2  6652  limsssuc  6658  dfom2  6675  relcnvexb  6721  dfsmo2  7010  omord  7209  nneob  7293  pw2f1olem  7614  sucdom  7708  fieq0  7873  hartogslem1  7959  rankr1ag  8211  rankeq0b  8269  fidomtri  8365  fidomtri2  8366  isfin2-2  8690  enfin2i  8692  isfin3-2  8738  isf34lem6  8751  isfin1-2  8756  isfin1-3  8757  isfin7-2  8767  axgroth6  9195  ltsonq  9336  ltexnq  9342  znegclb  10897  rpneg  11251  nltpnft  11370  ngtmnft  11371  xrrebnd  11372  qextlt  11405  qextle  11406  iccneg  11644  fzsn  11729  fz1sbc  11758  fzofzp1b  11891  ceilidz  11961  fleqceilz  11963  hashclb  12415  hashnncl  12422  hashfun  12482  reim0b  13037  rexanre  13264  rexuzre  13270  lo1resb  13472  o1resb  13474  dvdsext  14124  pceq0  14481  pc11  14490  pcz  14491  ramtcl  14615  cshwsiun  14671  pospo  15805  oduposb  15968  cnvpsb  16045  tsrlemax  16052  issubg2  16418  issubg4  16422  ghmmhmb  16480  pmtrmvd  16683  mndodcong  16768  issubrg2  17647  lpigen  18102  cyggic  18787  ip2eq  18864  maducoeval2  19312  eltg3  19633  bastop  19653  0top  19655  iscld3  19735  isclo2  19759  cnprest  19960  dfcon2  20089  comppfsc  20202  cmphaushmeo  20470  reghaus  20495  nrmhaus  20496  fbun  20510  fsubbas  20537  ufileu  20589  uffix  20591  txflf  20676  fclsrest  20694  flimfnfcls  20698  ptcmplem2  20722  tgpt1  20785  tgpt0  20786  isngp2  21286  nrgdomn  21349  nmhmcn  21772  iscmet3  21901  limcflf  22454  ply1nzb  22692  coe11  22819  dgreq0  22831  sqf11  23614  sqff1o  23657  lgsabs1  23810  lgsquadlem2  23831  usgrafilem2  24617  cusgrafilem3  24686  iswlkg  24729  wwlkn0s  24910  isclwlkg  24960  el2wlksoton  25083  el2spthsoton  25084  vdiscusgra  25126  elghomlem2OLD  25565  nmobndi  25891  hmopadj2  27061  mdslle1i  27437  mdslle2i  27438  relfi  27676  ssrelf  27684  eldmgm  28831  rescon  28958  cvmsval  28978  elmrsubrn  29147  funsseq  29442  brcolinear  29940  outsideofeu  30012  lineunray  30028  wl-sb5nae  30250  wl-ax11-lem2  30269  heicant  30292  nn0prpw  30384  cover2  30447  eqfnun  30455  isbndx  30521  isbnd2  30522  equivbnd2  30531  prdsbnd2  30534  isdrngo3  30605  ceqsex3OLD  30844  wepwsolem  31229  pm11.71  31547  pm14.122b  31574  pm14.123b  31577  iotavalb  31581  climreeq  31861  rexrsb  32416  reuan  32427  afv0nbfvbi  32478  dfafn5b  32488  zob  32551  zeo2ALTV  32585  fundmfibi  32704  f1dmvrnfibi  32705  elfz2z  32724  usgfislem2  32836  usgfisALTlem2  32840  nnlog2ge0lt1  33460  bnj1173  34478  bj-19.3t  34672  bj-sb3b  34810  bj-sngltag  34961  bj-elid2  35020  bj-inftyexpiinj  35031  riotaclbgBAD  35101  lssatle  35156  opcon3b  35337  cdlemk33N  37051  cdlemk34  37052  rp-fakeimass  38169  intimag  38203
  Copyright terms: Public domain W3C validator