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

Theorem impbid2 209
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 208 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
43bicomd 206 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  biimt  341  biorf  411  biorfi  413  pm4.72  892  biort  912  bimsc1  955  ax13b  1885  cgsexg  3092  cgsex2g  3093  cgsex4g  3094  elab3gf  3202  abidnf  3219  elsnc2g  4010  difsn  4119  eqsn  4146  prel12  4165  elpreqprb  4176  dfnfc2  4230  intmin4  4278  dfiin2g  4325  elpw2g  4580  ssrel  4942  ssrel2  4944  ssrelrel  4954  releldmb  5088  relelrnb  5089  cnveqb  5310  dmsnopg  5326  relcnvtr  5374  ord0eln0  5496  f1ocnvb  5850  ffvresb  6078  soisores  6243  riotaclb  6314  fnoprabg  6424  difex2  6625  dfwe2  6635  ordpwsuc  6669  ordunisuc2  6698  limsssuc  6704  dfom2  6721  relcnvexb  6768  dfsmo2  7092  omord  7295  nneob  7379  pw2f1olem  7702  sucdom  7795  fundmfibi  7881  f1dmvrnfibi  7884  fieq0  7961  hartogslem1  8083  rankr1ag  8299  rankeq0b  8357  fidomtri  8453  fidomtri2  8454  isfin2-2  8775  enfin2i  8777  isfin3-2  8823  isf34lem6  8836  isfin1-2  8841  isfin1-3  8842  isfin7-2  8852  axgroth6  9279  ltsonq  9420  ltexnq  9426  znegclb  11003  rpneg  11361  nltpnft  11490  ngtmnft  11491  xrrebnd  11492  qextlt  11525  qextle  11526  iccneg  11782  fzsn  11869  fz1sbc  11899  fzofzp1b  12040  ceilidz  12111  fleqceilz  12113  hashclb  12572  hashnncl  12579  hashfun  12642  reim0b  13231  rexanre  13458  rexuzre  13464  lo1resb  13677  o1resb  13679  dvdsext  14405  ncoprmgcdne1b  14704  pceq0  14869  pc11  14878  pcz  14879  ramtcl  15013  ramtclOLD  15014  cshwsiun  15119  pospo  16268  oduposb  16431  cnvpsb  16508  tsrlemax  16515  issubg2  16881  issubg4  16885  ghmmhmb  16943  pmtrmvd  17146  mndodcong  17240  issubrg2  18077  lpigen  18529  cyggic  19192  ip2eq  19269  maducoeval2  19714  eltg3  20026  bastop  20046  0top  20048  iscld3  20129  isclo2  20153  cnprest  20354  dfcon2  20483  comppfsc  20596  cmphaushmeo  20864  reghaus  20889  nrmhaus  20890  fbun  20904  fsubbas  20931  ufileu  20983  uffix  20985  txflf  21070  fclsrest  21088  flimfnfcls  21092  ptcmplem2  21117  tgpt1  21181  tgpt0  21182  isngp2  21660  nrgdomn  21723  nmhmcn  22183  iscmet3  22312  limcflf  22885  ply1nzb  23120  coe11  23256  dgreq0  23268  eldmgm  23996  sqf11  24115  sqff1o  24158  lgsabs1  24311  lgsquadlem2  24332  usgrafilem2  25189  cusgrafilem3  25258  iswlkg  25301  wwlkn0s  25482  isclwlkg  25532  el2wlksoton  25655  el2spthsoton  25656  vdiscusgra  25698  elghomlem2OLD  26139  nmobndi  26465  hmopadj2  27643  mdslle1i  28019  mdslle2i  28020  relfi  28262  ssrelf  28270  bnj1173  29860  rescon  30018  cvmsval  30038  elmrsubrn  30207  funsseq  30458  brcolinear  30875  outsideofeu  30947  lineunray  30963  nn0prpw  31028  bj-19.3t  31337  bj-sb3b  31464  bj-sngltag  31622  bj-elid2  31686  bj-inftyexpiinj  31696  wl-sb5nae  31932  wl-ax11-lem2  31961  poimirlem26  32011  poimirlem27  32012  heicant  32020  cover2  32085  eqfnun  32093  isbndx  32159  isbnd2  32160  equivbnd2  32169  prdsbnd2  32172  isdrngo3  32243  riotaclbgBAD  32571  lssatle  32626  opcon3b  32807  cdlemk33N  34521  cdlemk34  34522  wepwsolem  35945  rp-fakeimass  36201  cnvssb  36237  intimag  36293  pm11.71  36791  pm14.122b  36818  pm14.123b  36821  iotavalb  36825  climreeq  37731  rexrsb  38628  reuan  38639  afv0nbfvbi  38691  dfafn5b  38701  zob  38801  zeo2ALTV  38838  elfz2z  39097  issubgr2  39394  uhgrissubgr  39397  usgrfilem  39443  cusgrfilem3  39568  vdiscusgr  39618  usgfislem2  40030  usgfisALTlem2  40034  nnlog2ge0lt1  40650
  Copyright terms: Public domain W3C validator