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

Theorem biimprd 223
Description: Deduce a converse implication from a logical equivalence. (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 221 1  |-  ( ph  ->  ( ch  ->  ps ) )
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:  syl6bir  229  mpbird  232  sylibrd  234  sylbird  235  con4bid  293  mtbid  300  mtbii  302  imbi1d  317  biimpar  485  prlem1  960  spfw  1755  cbvalw  1757  alcomiw  1760  ax12v  1804  nfimd  1864  axc11nlem  1885  cbval  1994  axc11nlemOLD  2021  axc16i  2037  equvini  2060  axc16gALT  2079  sbequi  2089  sb9iOLD  2151  dral1-o  2226  ax16g-o  2257  eqrdav  2465  cleqhOLD  2583  pm13.18  2778  rspcimdv  3215  rspcedv  3218  moi2  3284  moi  3286  eqrd  3522  sspsstr  3609  reusv6OLD  4658  reusv7OLD  4659  ralxfrd  4661  ralxfr2d  4663  isso2i  4832  wefrc  4873  oneqmini  4929  ordsssuc2  4966  ordtri2or  4973  elres  5307  sotri3  5395  2elresin  5690  f1ocnv  5826  tz6.12c  5883  fveqres  5898  fvun1  5936  dffo4  6035  fconst5  6116  fnprb  6117  fnprOLD  6118  isores3  6217  f1owe  6235  weniso  6236  ndmovordi  6448  orduniorsuc  6643  ordzsl  6658  tfinds  6672  f1oweALT  6765  fnse  6897  tposfo2  6975  issmo2  7017  iordsmo  7025  smoel2  7031  tz7.48lem  7103  oawordeulem  7200  om00  7221  omlimcl  7224  odi  7225  nnawordi  7267  fiint  7793  fipreima  7822  dffi2  7879  suplub2  7917  wemapsolem  7971  unwdomg  8006  inf3lem3  8043  trcl  8155  fidomtri  8370  prdom2  8380  cardaleph  8466  ackbij1lem16  8611  coflim  8637  coftr  8649  infpssrlem4  8682  isfin7-2  8772  axdc3lem2  8827  axdc3lem4  8829  brdom6disj  8906  entric  8928  fpwwe2lem12  9015  inatsk  9152  grur1a  9193  indpi  9281  reclem3pr  9423  supsrlem  9484  lelttr  9671  dedekindle  9740  fimaxre  10486  nnmulcl  10555  arch  10788  nnnegz  10863  zeo  10942  uzm1  11108  negn0  11164  rpneg  11245  xrlttri  11341  xrlelttr  11355  iccid  11570  icoshft  11638  fzen  11699  fzm1  11754  elfz2nn0  11764  elfzom1p1elfzo  11859  fleqceilz  11945  zmodidfzoimp  11990  hasheqf1oi  12388  hashnfinnn0  12396  swrd0  12617  swrdccatin12lem2  12673  swrdccat  12677  swrdccat3blem  12679  repswswrd  12715  max0add  13102  abslt  13106  absle  13107  rexuzre  13144  caurcvg  13458  caucvg  13460  dvdsval2  13846  negdvdsb  13857  muldvds2  13866  smuval2  13987  smupvallem  13988  rplpwr  14049  alginv  14059  algfx  14064  prmgt1  14091  rpexp1i  14117  qnumdencl  14127  phiprmpw  14161  prmdiveq  14171  pcmpt  14266  infpnlem1  14283  imasaddfnlem  14779  plelttr  15455  lubval  15467  lublecllem  15471  glbval  15480  mrcmndind  15807  mndodconglem  16361  elfrlmbasn0  18563  mavmulsolcl  18820  slesolex  18951  fvmptnn04if  19117  chfacfisf  19122  chfacfisfcpmat  19123  cnpnei  19531  uncon  19696  kqsat  19967  isr0  19973  qtophmeo  20053  trufil  20146  alexsubALT  20286  cnextcn  20302  ucnima  20519  iducn  20521  bl2in  20638  addcnlem  21103  rescncf  21136  ovoliunlem2  21649  voliun  21699  mbflimsup  21808  itgcn  21984  dvdsq1p  22296  aalioulem2  22463  recosf1o  22655  logrec  22879  xrlimcnp  23026  basellem4  23085  bposlem1  23287  bposlem5  23291  lgsdchrval  23350  pntlem3  23522  brbtwn2  23884  axbtwnid  23918  usgraedgprv  24052  usgraedgrnv  24053  usgrafisinds  24089  iswlkg  24200  isclwlkg  24431  clwlkisclwwlklem2a1  24455  clwwisshclww  24483  clwlksizeeq  24528  eupai  24643  numclwwlkovf2ex  24763  numclwwlk2lem1  24779  numclwwlk5lem  24788  frgrareggt1  24793  friendship  24799  elghomlem2  25040  blocn2  25399  htthlem  25510  axhcompl-zf  25591  spanuni  26138  spansncol  26162  spansneleq  26164  elspansn5  26168  idcnop  26576  pjnormssi  26763  dmdmd  26895  bian1d  27042  ifeqeqx  27093  supxrnemnf  27251  rexdiv  27290  xrstos  27329  xrge0omnd  27363  cnre2csqlem  27528  fsumcvg4  27568  lmxrge0  27570  qqhval2lem  27598  esumpr2  27714  esumcvg  27732  issgon  27763  measxun2  27821  measres  27833  measdivcstOLD  27835  measdivcst  27836  elorrvc  28042  signsply0  28148  erdsze2lem2  28288  cvmsval  28351  ghomgsg  28508  ghomf1olem  28509  fprod2dlem  28687  fundmpss  28773  dfon2lem3  28794  frmin  28899  poseq  28910  soseq  28911  wfrlem5  28924  wfrlem12  28931  frrlem5  28968  frrlem11  28976  nobndup  29037  nobnddown  29038  dfrdg4  29177  cgrtriv  29229  btwntriv2  29239  ifscgr  29271  lineext  29303  btwnconn1lem12  29325  colinbtwnle  29345  ontgval  29473  onsucconi  29479  wl-nfs1t  29568  finixpnum  29615  ltflcei  29620  itg2addnclem  29643  areacirclem2  29685  areacirclem5  29688  areacirc  29689  elicc3  29712  comppfsc  29779  nninfnub  29847  prdstotbnd  29893  heiborlem4  29913  heibor  29920  grpokerinj  29950  isidlc  30015  prtlem17  30221  elrfirn2  30232  rencldnfilem  30358  sdrgacs  30755  cncfiooicclem1  31232  stoweidlem35  31335  stoweidlem48  31348  rexrsb  31641  funbrafv  31710  rlimdmafv  31729  fzoopth  31809  2ffzoeq  31810  usgedgvadf1lem2  31883  usgedgvadf1ALTlem2  31886  usgfis  31915  usgfisALT  31919  usgrafiedgALT  31920  mgm2mgm  31977  ellcoellss  32109  snelpwrVD  32711  en3lplem1VD  32723  en3lpVD  32725  orbi1rVD  32728  sbc3orgVD  32731  3impexpVD  32736  equncomVD  32748  trsbcVD  32757  trintALTVD  32760  trintALT  32761  csbingVD  32764  csbsngVD  32773  csbxpgVD  32774  csbrngVD  32776  csbfv12gALTVD  32779  relopabVD  32781  e2ebindVD  32792  bnj580  33050  bj-bibibi  33256  bj-cbvalv  33378  bj-axc11nlemv  33396  bj-cleqh  33439  bj-equsal  33480  bj-elid  33672  bj-finsumval0  33735  lsator0sp  33798  atlrelat1  34118  cvratlem  34217  diaintclN  35855  dibintclN  35964  cdlemn11pre  36007  dihord2pre  36022  dihintcl  36141  dochkrshp4  36186  lcfrlem9  36347  lcfrlem21  36360  mapdh8e  36581
  Copyright terms: Public domain W3C validator