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, 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 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  482  prlem1  946  spfw  1743  cbvalw  1745  alcomiw  1748  nfimd  1848  cbval  1968  axc11nlem  1995  axc16i  2011  equvini  2036  sbequi  2063  ax16gALT  2105  sb9iOLD  2130  dral1-o  2205  ax16g-o  2236  cleqh  2530  pm13.18  2673  rspcimdv  3063  rspcedv  3066  moi2  3129  moi  3131  eqrd  3362  sspsstr  3449  reusv6OLD  4491  reusv7OLD  4492  ralxfrd  4494  ralxfr2d  4496  isso2i  4660  wefrc  4701  oneqmini  4757  ordsssuc2  4794  ordtri2or  4801  elres  5133  sotri3  5216  2elresin  5510  f1ocnv  5641  tz6.12c  5697  fveqres  5712  fvun1  5750  dffo4  5847  fconst5  5922  fnprb  5923  fnprOLD  5924  isores3  6013  f1owe  6031  weniso  6032  ndmovordi  6243  orduniorsuc  6430  ordzsl  6445  tfinds  6459  f1oweALT  6550  fnse  6678  tposfo2  6757  issmo2  6796  iordsmo  6804  smoel2  6810  tz7.48lem  6882  abianfp  6900  oawordeulem  6981  om00  7002  omlimcl  7005  odi  7006  nnawordi  7048  fiint  7576  fipreima  7605  dffi2  7661  suplub2  7699  wemapsolem  7752  unwdomg  7787  inf3lem3  7824  trcl  7936  fidomtri  8151  prdom2  8161  cardaleph  8247  ackbij1lem16  8392  coflim  8418  coftr  8430  infpssrlem4  8463  isfin7-2  8553  axdc3lem2  8608  axdc3lem4  8610  brdom6disj  8687  entric  8709  fpwwe2lem12  8795  inatsk  8932  grur1a  8973  indpi  9063  reclem3pr  9205  supsrlem  9265  lelttr  9452  dedekindle  9521  fimaxre  10264  nnmulcl  10332  arch  10563  nnnegz  10636  zeo  10714  uzm1  10878  negn0  10928  rpneg  11007  xrlttri  11103  xrlelttr  11117  iccid  11332  icoshft  11393  fzen  11453  elfz2nn0  11466  fzm1  11523  fleqceilz  11676  zmodidfzoimp  11721  hasheqf1oi  12105  hashnfinnn0  12113  swrd0  12310  swrdccatin12lem2  12363  swrdccat  12367  swrdccat3blem  12369  repswswrd  12405  max0add  12782  abslt  12785  absle  12786  rexuzre  12823  caurcvg  13137  caucvg  13139  dvdsval2  13520  negdvdsb  13531  muldvds2  13540  smuval2  13660  smupvallem  13661  rplpwr  13722  alginv  13732  algfx  13737  prmgt1  13764  rpexp1i  13789  qnumdencl  13799  phiprmpw  13833  prmdiveq  13843  pcmpt  13936  infpnlem1  13953  imasaddfnlem  14448  plelttr  15124  lubval  15136  lublecllem  15140  glbval  15149  mrcmndind  15475  mndodconglem  16023  elfrlmbasn0  18031  mavmulsolcl  18203  slesolex  18329  cnpnei  18709  uncon  18874  kqsat  19145  isr0  19151  qtophmeo  19231  trufil  19324  alexsubALT  19464  cnextcn  19480  ucnima  19697  iducn  19699  bl2in  19816  addcnlem  20281  rescncf  20314  ovoliunlem2  20827  voliun  20876  mbflimsup  20985  itgcn  21161  dvdsq1p  21516  aalioulem2  21683  recosf1o  21875  logrec  22099  xrlimcnp  22246  basellem4  22305  bposlem1  22507  bposlem5  22511  lgsdchrval  22570  pntlem3  22742  brbtwn2  22973  axbtwnid  23007  usgraedgprv  23117  usgraedgrnv  23118  usgrafisinds  23148  eupai  23410  elghomlem2  23671  blocn2  24030  htthlem  24141  axhcompl-zf  24222  spanuni  24769  spansncol  24793  spansneleq  24795  elspansn5  24799  idcnop  25207  pjnormssi  25394  dmdmd  25526  bian1d  25673  ifeqeqx  25725  supxrnemnf  25878  rexdiv  25923  xrstos  25962  xrge0omnd  25997  cnre2csqlem  26193  fsumcvg4  26233  lmxrge0  26235  qqhval2lem  26263  esumpr2  26370  esumcvg  26388  issgon  26419  measxun2  26477  measres  26489  measdivcstOLD  26491  measdivcst  26492  elorrvc  26693  signsply0  26799  erdsze2lem2  26939  cvmsval  27002  ghomgsg  27158  ghomf1olem  27159  fprod2dlem  27337  fundmpss  27423  dfon2lem3  27444  frmin  27549  poseq  27560  soseq  27561  wfrlem5  27574  wfrlem12  27581  frrlem5  27618  frrlem11  27626  nobndup  27687  nobnddown  27688  dfrdg4  27827  cgrtriv  27879  btwntriv2  27889  ifscgr  27921  lineext  27953  btwnconn1lem12  27975  colinbtwnle  27995  ontgval  28124  onsucconi  28130  wl-nfs1t  28213  finixpnum  28255  ltflcei  28260  itg2addnclem  28284  areacirclem2  28326  areacirclem5  28329  areacirc  28330  elicc3  28353  comppfsc  28420  nninfnub  28488  prdstotbnd  28534  heiborlem4  28554  heibor  28561  grpokerinj  28591  isidlc  28656  prtlem17  28863  elrfirn2  28874  rencldnfilem  29001  sdrgacs  29400  stoweidlem35  29673  stoweidlem48  29686  rexrsb  29836  funbrafv  29907  rlimdmafv  29926  fzoopth  30056  2ffzoeq  30057  elfzom1p1elfzo  30058  iswlkg  30128  isclwlkg  30263  clwlkisclwwlklem2a1  30284  clwwisshclww  30314  clwlksizeeq  30368  numclwwlkovf2ex  30522  numclwwlk2lem1  30538  numclwwlk5lem  30547  frgrareggt1  30552  friendship  30558  ellcoellss  30675  snelpwrVD  31266  en3lplem1VD  31278  en3lpVD  31280  orbi1rVD  31283  sbc3orgVD  31286  3impexpVD  31291  equncomVD  31303  trsbcVD  31312  trintALTVD  31315  trintALT  31316  csbingVD  31319  csbsngVD  31328  csbxpgVD  31329  csbrngVD  31331  csbfv12gALTVD  31334  relopabVD  31336  e2ebindVD  31347  bnj580  31605  bj-cbvalv  31860  bj-axc11nlemv  31878  bj-cleqh  31912  bj-equsal  31951  bj-finsumval0  32156  lsator0sp  32216  atlrelat1  32536  cvratlem  32635  diaintclN  34273  dibintclN  34382  cdlemn11pre  34425  dihord2pre  34440  dihintcl  34559  dochkrshp4  34604  lcfrlem9  34765  lcfrlem21  34778  mapdh8e  34999
  Copyright terms: Public domain W3C validator