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  876  biort  896  bimsc1  938  ax13b  1791  cgsexg  3128  cgsex2g  3129  cgsex4g  3130  elab3gf  3237  abidnf  3254  elsnc2g  4044  difsn  4149  eqsn  4176  prel12  4192  dfnfc2  4252  intmin4  4301  dfiin2g  4348  elpw2g  4600  ord0eln0  4922  ssrel  5081  ssrel2  5083  ssrelrel  5093  releldmb  5227  relelrnb  5228  cnveqb  5452  dmsnopg  5469  relcnvtr  5517  f1ocnvb  5819  ffvresb  6047  soisores  6208  riotaclb  6280  fnoprabg  6388  difex2  6592  dfwe2  6602  ordpwsuc  6635  ordunisuc2  6664  limsssuc  6670  dfom2  6687  relcnvexb  6733  dfsmo2  7020  omord  7219  nneob  7303  pw2f1olem  7623  sucdom  7717  fieq0  7883  hartogslem1  7970  rankr1ag  8223  rankeq0b  8281  fidomtri  8377  fidomtri2  8378  isfin2-2  8702  enfin2i  8704  isfin3-2  8750  isf34lem6  8763  isfin1-2  8768  isfin1-3  8769  isfin7-2  8779  axgroth6  9209  ltsonq  9350  ltexnq  9356  znegclb  10908  rpneg  11260  nltpnft  11378  ngtmnft  11379  xrrebnd  11380  qextlt  11413  qextle  11414  iccneg  11652  fzsn  11736  fz1sbc  11765  fzofzp1b  11892  ceilidz  11961  fleqceilz  11963  hashclb  12412  hashnncl  12418  hashfun  12477  reim0b  12934  rexanre  13161  rexuzre  13167  lo1resb  13369  o1resb  13371  dvdsext  14019  pceq0  14376  pc11  14385  pcz  14386  ramtcl  14510  cshwsiun  14566  pospo  15582  oduposb  15745  cnvpsb  15822  tsrlemax  15829  issubg2  16195  issubg4  16199  ghmmhmb  16257  pmtrmvd  16460  mndodcong  16545  issubrg2  17428  lpigen  17883  cyggic  18589  ip2eq  18666  maducoeval2  19120  eltg3  19441  bastop  19461  0top  19463  iscld3  19543  isclo2  19567  cnprest  19768  dfcon2  19898  comppfsc  20011  cmphaushmeo  20279  reghaus  20304  nrmhaus  20305  fbun  20319  fsubbas  20346  ufileu  20398  uffix  20400  txflf  20485  fclsrest  20503  flimfnfcls  20507  ptcmplem2  20531  tgpt1  20594  tgpt0  20595  isngp2  21095  nrgdomn  21158  nmhmcn  21581  iscmet3  21710  limcflf  22263  ply1nzb  22501  coe11  22628  dgreq0  22640  sqf11  23391  sqff1o  23434  lgsabs1  23587  lgsquadlem2  23608  usgrafilem2  24390  cusgrafilem3  24459  iswlkg  24502  wwlkn0s  24683  isclwlkg  24733  el2wlksoton  24856  el2spthsoton  24857  vdiscusgra  24899  elghomlem2OLD  25342  nmobndi  25668  hmopadj2  26838  mdslle1i  27214  mdslle2i  27215  relfi  27437  ssrelf  27444  eldmgm  28542  rescon  28669  cvmsval  28689  elmrsubrn  28858  funsseq  29175  brcolinear  29685  outsideofeu  29757  lineunray  29773  wl-sb5nae  29983  wl-ax11-lem2  30002  heicant  30025  nn0prpw  30117  cover2  30180  eqfnun  30188  isbndx  30254  isbnd2  30255  equivbnd2  30264  prdsbnd2  30267  isdrngo3  30338  ceqsex3OLD  30577  wepwsolem  30963  pm11.71  31257  pm14.122b  31284  pm14.123b  31287  iotavalb  31291  climreeq  31573  rexrsb  32128  reuan  32139  afv0nbfvbi  32190  dfafn5b  32200  fundmfibi  32265  f1dmvrnfibi  32266  elfz2z  32285  usgfislem2  32399  usgfisALTlem2  32403  bnj1173  33926  bj-19.3t  34135  bj-sb3b  34273  bj-sngltag  34424  bj-elid2  34475  bj-inftyexpiinj  34487  riotaclbgBAD  34560  lssatle  34615  opcon3b  34796  cdlemk33N  36510  cdlemk34  36511  rp-fakeimass  37574
  Copyright terms: Public domain W3C validator