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

Theorem biimprd 231
Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 203 and biimpri 211. (Contributed by NM, 11-Jan-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 22 . 2  |-  ( ch 
->  ch )
2 biimprd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibr 229 1  |-  ( ph  ->  ( ch  ->  ps ) )
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:  syl6bir  237  mpbird  240  sylibrd  242  sylbird  243  con4bid  300  mtbid  307  mtbii  309  imbi1d  324  biimpar  493  prlem1  974  alexbii  1713  spfw  1883  cbvalw  1885  alcomiw  1888  aevlem0  1896  axc11nlemOLD2  1902  ax12vOLDOLD  1954  nfimd  2020  axc11nlemOLD  2041  cbvalv1  2083  cbval  2127  axc11nlemALT  2156  axc16i  2171  equvini  2195  axc16gALT  2216  sbequi  2224  eqrdav  2470  pm13.18  2724  rspcimdv  3137  rspcedv  3140  moi2  3207  moi  3209  eqrd  3436  sspsstr  3524  eqoreldif  4004  ralxfrd  4612  ralxfr2d  4614  isso2i  4792  wefrc  4833  elres  5146  sotri3  5236  oneqmini  5481  ordsssuc2  5518  ordtri2or  5525  2elresin  5697  f1ocnv  5840  tz6.12c  5898  fveqres  5913  fvun1  5951  dffo4  6053  fconst5  6138  fnprb  6139  fntpb  6140  isores3  6244  f1owe  6262  weniso  6263  ndmovordi  6479  orduniorsuc  6676  ordzsl  6691  tfinds  6705  f1oweALT  6796  fnse  6932  tposfo2  7014  wfrlem5  7058  wfrlem12  7065  issmo2  7086  iordsmo  7094  smoel2  7100  tz7.48lem  7176  oawordeulem  7273  om00  7294  omlimcl  7297  odi  7298  nnawordi  7340  fiint  7866  fipreima  7898  dffi2  7955  suplub2  7993  wemapsolem  8083  unwdomg  8117  inf3lem3  8153  trcl  8230  fidomtri  8445  prdom2  8455  cardaleph  8538  ackbij1lem16  8683  coflim  8709  coftr  8721  infpssrlem4  8754  isfin7-2  8844  axdc3lem2  8899  axdc3lem4  8901  brdom6disj  8978  entric  9000  fpwwe2lem12  9084  inatsk  9221  grur1a  9262  indpi  9350  reclem3pr  9492  supsrlem  9553  lelttr  9742  dedekindle  9816  negn0  10069  fimaxre  10573  nnmulcl  10654  arch  10890  nnnegz  10964  zeo  11044  uzm1  11213  rpneg  11355  xrlttri  11461  xrlelttr  11476  iccid  11706  icoshft  11780  fzen  11842  elfz2nn0  11911  elfzom1p1elfzo  12022  fleqceilz  12114  zmodidfzoimp  12160  modsumfzodifsn  12196  hasheqf1oi  12572  hashnfinnn0  12580  swrd0  12844  swrdccatin12lem2  12899  swrdccat  12903  swrdccat3blem  12905  repswswrd  12941  trclublem  13134  max0add  13450  abslt  13454  absle  13455  rexuzre  13492  caurcvg  13819  caurcvgOLD  13820  caucvg  13822  dvdsval2  14385  negdvdsb  14396  muldvds2  14405  smuval2  14535  smupvallem  14536  rplpwr  14603  alginv  14613  algfx  14618  prmgt1  14722  coprmgcdb  14733  rpexp1i  14752  qnumdencl  14767  phiprmpw  14803  prmdiveq  14813  pcmpt  14916  infpnlem1  14933  prmgaplem3  15102  prmgaplem8  15107  imasaddfnlem  15512  plelttr  16296  lubval  16308  lublecllem  16312  glbval  16321  mrcmndind  16691  mndodconglem  17268  elfrlmbasn0  19402  mavmulsolcl  19653  slesolex  19784  fvmptnn04if  19950  chfacfisf  19955  chfacfisfcpmat  19956  cnpnei  20357  uncon  20521  comppfsc  20624  kqsat  20823  isr0  20829  qtophmeo  20909  trufil  21003  alexsubALT  21144  cnextcn  21160  ucnima  21374  iducn  21376  bl2in  21493  addcnlem  21974  rescncf  22007  ovoliunlem2  22534  voliun  22586  mbflimsup  22702  mbflimsupOLD  22703  itgcn  22879  dvdsq1p  23190  aalioulem2  23368  recosf1o  23563  logrec  23779  xrlimcnp  23973  basellem4  24089  bposlem1  24291  bposlem5  24295  lgsdchrval  24354  pntlem3  24526  brbtwn2  25014  axbtwnid  25048  usgraedgprv  25182  usgraedgrnv  25183  usgrafisinds  25220  iswlkg  25331  wwlkextinj  25537  isclwlkg  25562  clwlkisclwwlklem2a1  25586  clwwisshclww  25614  clwlksizeeq  25659  eupai  25774  numclwwlkovf2ex  25893  numclwwlk2lem1  25909  numclwwlk5lem  25918  frgrareggt1  25923  friendship  25929  elghomlem2OLD  26171  blocn2  26530  htthlem  26651  axhcompl-zf  26732  spanuni  27278  spansncol  27302  spansneleq  27304  elspansn5  27308  idcnop  27715  pjnormssi  27902  dmdmd  28034  bian1d  28181  ifeqeqx  28236  supxrnemnf  28429  rexdiv  28470  xrstos  28516  xrge0omnd  28548  cnre2csqlem  28790  fsumcvg4  28830  lmxrge0  28832  qqhval2lem  28859  esumpr2  28962  esumcvg  28981  issgon  29019  measxun2  29106  measres  29118  measdivcstOLD  29120  measdivcst  29121  elorrvc  29369  signsply0  29512  bnj580  29796  erdsze2lem2  29999  cvmsval  30061  ghomgsg  30383  ghomf1olem  30384  fundmpss  30478  dfon2lem3  30502  frmin  30551  poseq  30562  soseq  30563  frrlem5  30589  frrlem11  30597  nobndup  30660  nobnddown  30661  dfrdg4  30789  cgrtriv  30840  btwntriv2  30850  ifscgr  30882  lineext  30914  btwnconn1lem12  30936  colinbtwnle  30956  elicc3  31044  ontgval  31162  onsucconi  31168  bj-bibibi  31234  bj-cbvexw  31337  bj-axc11nlemv  31413  bj-equsal  31494  bj-elid  31710  bj-finsumval0  31772  relowlssretop  31836  sucneqond  31838  finxpsuc  31860  wl-nfs1t  31941  finixpnum  31994  ltflcei  31997  poimirlem23  32027  poimirlem24  32028  poimirlem27  32031  poimirlem32  32036  itg2addnclem  32057  areacirclem2  32097  areacirclem5  32100  areacirc  32101  nninfnub  32144  prdstotbnd  32190  heiborlem4  32210  heibor  32217  grpokerinj  32247  isidlc  32312  prtlem17  32512  dral1-o  32538  axc16g-o  32569  lsator0sp  32638  atlrelat1  32958  cvratlem  33057  diaintclN  34697  dibintclN  34806  cdlemn11pre  34849  dihord2pre  34864  dihintcl  34983  dochkrshp4  35028  lcfrlem9  35189  lcfrlem21  35202  mapdh8e  35423  elrfirn2  35609  rencldnfilem  35734  sdrgacs  36138  refimssco  36284  rtrclex  36295  intimasn  36320  ss2iundf  36322  ov2ssiunov2  36363  comptiunov2i  36369  iunrelexpuztr  36382  snelpwrVD  37290  en3lplem1VD  37302  en3lpVD  37304  orbi1rVD  37307  sbc3orgVD  37310  3impexpVD  37315  equncomVD  37328  trsbcVD  37337  trintALTVD  37340  trintALT  37341  csbingVD  37344  csbsngVD  37353  csbxpgVD  37354  csbrngVD  37356  csbfv12gALTVD  37359  relopabVD  37361  e2ebindVD  37372  stoweidlem35  38008  stoweidlem48  38021  rexrsb  38735  funbrafv  38805  rlimdmafv  38824  fzopredsuc  38865  iccpartlt  38883  nnsum3primesle9  39034  wtgoldbnnsum4prm  39042  bgoldbnnsum3prm  39044  pfxccatin12lem2  39112  funopsn  39164  fzoopth  39208  2ffzoeq  39209  umgredgprv  39352  umgrpredgav  39391  usgredgprvALT  39440  fusgrfisstep  39559  fusgrfis  39560  nbupgr  39576  nbumgrvtx  39578  1wlkp1lem8  39876  upgr2pthnlp  39925  isclWlkb  39960  crctisclwlk  39977  cyclnsPth  39982  eucrctshift  40155  eucrct2eupth  40157  usgedgvadf1lem2  40234  usgedgvadf1ALTlem2  40237  usgfis  40266  usgfisALT  40270  usgrafiedgALT  40271  mgm2mgm  40371  2zrngnmlid  40457  2zrngnmrid  40458  ellcoellss  40736  nneop  40841  fldivexpfllog2  40884  digexp  40926
  Copyright terms: Public domain W3C validator