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

Theorem biimprd 215
Description: Deduce a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimprd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimprd  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem biimprd
StepHypRef Expression
1 id 20 . 2  |-  ( ch 
->  ch )
2 biimprd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibr 213 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl6bir  221  mpbird  224  sylibrd  226  sylbird  227  con4bid  285  mtbid  292  mtbii  294  imbi1d  309  biimpar  472  prlem1  929  spfw  1703  spwOLD  1707  cbvalw  1714  cbvalvwOLD  1716  alcomiw  1718  nfimd  1827  speivOLD  1967  cbval  1982  ax10lem2  2023  ax10lem2OLD  2026  ax10lem4OLD  2030  dral1OLD  2054  ax16i  2130  a16gALT  2133  sbequi  2136  sbequiOLD  2137  sb9i  2169  dral1-o  2230  a16g-o  2262  cleqh  2527  pm13.18  2665  rspcimdv  3040  rspcedv  3043  moi2  3102  moi  3104  eqrd  3353  sspsstr  3439  isso2i  4522  wefrc  4563  oneqmini  4619  ordsssuc2  4656  ordtri2or  4663  reusv6OLD  4720  reusv7OLD  4721  ralxfrd  4723  ralxfr2d  4725  orduniorsuc  4796  ordzsl  4811  tfinds  4825  elres  5167  sotri3  5250  2elresin  5542  f1ocnv  5673  tz6.12c  5736  fveqres  5750  fvun1  5780  dffo4  5871  fconst5  5935  fnpr  5936  fnprOLD  5937  isores3  6041  f1owe  6059  f1oweALT  6060  weniso  6061  ndmovordi  6224  fnse  6449  tposfo2  6488  issmo2  6597  iordsmo  6605  smoel2  6611  tz7.48lem  6684  abianfp  6702  oawordeulem  6783  om00  6804  omlimcl  6807  odi  6808  nnawordi  6850  fiint  7369  fipreima  7398  dffi2  7414  suplub2  7450  wemapso2lem  7503  unwdomg  7536  inf3lem3  7569  trcl  7648  fidomtri  7864  prdom2  7874  cardaleph  7954  ackbij1lem16  8099  coflim  8125  coftr  8137  infpssrlem4  8170  isfin7-2  8260  axdc3lem2  8315  axdc3lem4  8317  brdom6disj  8394  entric  8416  fpwwe2lem12  8500  inatsk  8637  grur1a  8678  indpi  8768  reclem3pr  8910  supsrlem  8970  lelttr  9149  fimaxre  9939  nnmulcl  10007  arch  10202  nnnegz  10269  zeo  10339  uzm1  10500  negn0  10546  rpneg  10625  xrlttri  10716  xrlelttr  10730  iccid  10945  icoshft  11003  fzen  11056  elfz2nn0  11066  fzm1  11110  hasheqf1oi  11618  hashnfinnn0  11626  max0add  12098  abslt  12101  absle  12102  rexuzre  12139  caurcvg  12453  caucvg  12455  dvdsval2  12838  negdvdsb  12849  muldvds2  12858  smuval2  12977  smupvallem  12978  rplpwr  13039  alginv  13049  algfx  13054  rpexp1i  13104  qnumdencl  13114  phiprmpw  13148  prmdiveq  13158  pcmpt  13244  infpnlem1  13261  imasaddfnlem  13736  plelttr  14412  lubid  14422  mndodconglem  15162  cnpnei  17311  uncon  17475  kqsat  17746  isr0  17752  qtophmeo  17832  trufil  17925  alexsubALT  18065  cnextcn  18081  ucnima  18294  iducn  18296  bl2in  18413  addcnlem  18877  rescncf  18910  ovoliunlem2  19382  voliun  19431  mbflimsup  19541  itgcn  19717  dvdsq1p  20066  aalioulem2  20233  recosf1o  20420  logrec  20644  xrlimcnp  20790  basellem4  20849  bposlem1  21051  bposlem5  21055  lgsdchrval  21114  pntlem3  21286  usgraedgprv  21379  usgraedgrnv  21380  usgrafisinds  21410  eupai  21672  elghomlem2  21933  blocn2  22292  htthlem  22403  axhcompl-zf  22484  spanuni  23029  spansncol  23053  spansneleq  23055  elspansn5  23059  idcnop  23467  pjnormssi  23654  dmdmd  23786  bian1d  23933  ifeqeqx  23984  supxrnemnf  24110  rexdiv  24155  xrstos  24184  cnre2csqlem  24291  lmxrge0  24320  qqhval2lem  24348  esumpr2  24441  esumcvg  24459  issgon  24489  measxun2  24547  measres  24559  measdivcstOLD  24561  measdivcst  24562  elorrvc  24704  erdsze2lem2  24873  cvmsval  24936  ghomgsg  25087  ghomf1olem  25088  dedekindle  25171  fprod2dlem  25288  fundmpss  25372  dfon2lem3  25391  frmin  25492  poseq  25503  soseq  25504  wfrlem5  25510  wfrlem10  25515  wfrlem12  25517  frrlem5  25535  frrlem11  25543  nobndup  25604  nobnddown  25605  dfrdg4  25740  brbtwn2  25787  axbtwnid  25821  cgrtriv  25879  btwntriv2  25889  ifscgr  25921  lineext  25953  btwnconn1lem12  25975  colinbtwnle  25995  ontgval  26124  onsucconi  26130  ltflcei  26182  itg2addnclem  26197  areacirclem4  26225  areacirclem6  26228  areacirc  26229  elicc3  26252  comppfsc  26319  nninfnub  26387  prdstotbnd  26435  heiborlem4  26455  heibor  26462  grpokerinj  26492  isidlc  26557  prtlem17  26657  elrfirn2  26682  rencldnfilem  26813  sdrgacs  27419  stoweidlem35  27693  stoweidlem48  27706  rexrsb  27856  funbrafv  27931  rlimdmafv  27950  swrd0  28044  swrdccat3b  28073  snelpwrVD  28695  en3lplem1VD  28707  en3lpVD  28709  orbi1rVD  28712  sbc3orgVD  28715  3impexpVD  28720  equncomVD  28732  trsbcVD  28741  trintALTVD  28744  trintALT  28745  csbingVD  28748  csbsngVD  28757  csbxpgVD  28758  csbrngVD  28760  csbfv12gALTVD  28763  relopabVD  28765  e2ebindVD  28776  bnj580  29036  ax10lem4NEW7  29223  dral1NEW7  29245  cbvalwwAUX7  29269  ax16iNEW7  29301  sbequiNEW7  29328  speivNEW7  29372  ax7w6AUX7  29398  cbvalOLD7  29455  a16gALTOLD7  29474  sb9iOLD7  29488  lsator0sp  29530  atlrelat1  29850  cvratlem  29949  diaintclN  31587  dibintclN  31696  cdlemn11pre  31739  dihord2pre  31754  dihintcl  31873  dochkrshp4  31918  lcfrlem9  32079  lcfrlem21  32092  mapdh8e  32313
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 178
  Copyright terms: Public domain W3C validator