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

Theorem biimprd 216
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 21 . 2  |-  ( ch 
->  ch )
2 biimprd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibr 214 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  syl6bir  222  mpbird  225  sylibrd  227  sylbird  228  con4bid  286  mtbid  293  mtbii  295  imbi1d  310  biimpar  473  prlem1  930  spfw  1704  spwOLD  1708  cbvalw  1715  cbvalvwOLD  1717  alcomiw  1719  nfimd  1828  speivOLD  1968  cbval  1983  ax10lem2  2024  ax10lem2OLD  2027  ax10lem4OLD  2031  ax16i  2052  dral1OLD  2059  sbequi  2111  sbequiOLD  2115  a16gALT  2157  sb9i  2171  dral1-o  2232  a16g-o  2264  cleqh  2534  pm13.18  2677  rspcimdv  3054  rspcedv  3057  moi2  3116  moi  3118  eqrd  3367  sspsstr  3453  isso2i  4536  wefrc  4577  oneqmini  4633  ordsssuc2  4671  ordtri2or  4678  reusv6OLD  4735  reusv7OLD  4736  ralxfrd  4738  ralxfr2d  4740  orduniorsuc  4811  ordzsl  4826  tfinds  4840  elres  5182  sotri3  5265  2elresin  5557  f1ocnv  5688  tz6.12c  5751  fveqres  5765  fvun1  5795  dffo4  5886  fconst5  5950  fnpr  5951  fnprOLD  5952  isores3  6056  f1owe  6074  f1oweALT  6075  weniso  6076  ndmovordi  6239  fnse  6464  tposfo2  6503  issmo2  6612  iordsmo  6620  smoel2  6626  tz7.48lem  6699  abianfp  6717  oawordeulem  6798  om00  6819  omlimcl  6822  odi  6823  nnawordi  6865  fiint  7384  fipreima  7413  dffi2  7429  suplub2  7467  wemapso2lem  7520  unwdomg  7553  inf3lem3  7586  trcl  7665  fidomtri  7881  prdom2  7891  cardaleph  7971  ackbij1lem16  8116  coflim  8142  coftr  8154  infpssrlem4  8187  isfin7-2  8277  axdc3lem2  8332  axdc3lem4  8334  brdom6disj  8411  entric  8433  fpwwe2lem12  8517  inatsk  8654  grur1a  8695  indpi  8785  reclem3pr  8927  supsrlem  8987  lelttr  9166  fimaxre  9956  nnmulcl  10024  arch  10219  nnnegz  10286  zeo  10356  uzm1  10517  negn0  10563  rpneg  10642  xrlttri  10733  xrlelttr  10747  iccid  10962  icoshft  11020  fzen  11073  elfz2nn0  11083  fzm1  11128  hasheqf1oi  11636  hashnfinnn0  11644  max0add  12116  abslt  12119  absle  12120  rexuzre  12157  caurcvg  12471  caucvg  12473  dvdsval2  12856  negdvdsb  12867  muldvds2  12876  smuval2  12995  smupvallem  12996  rplpwr  13057  alginv  13067  algfx  13072  rpexp1i  13122  qnumdencl  13132  phiprmpw  13166  prmdiveq  13176  pcmpt  13262  infpnlem1  13279  imasaddfnlem  13754  plelttr  14430  lubid  14440  mndodconglem  15180  cnpnei  17329  uncon  17493  kqsat  17764  isr0  17770  qtophmeo  17850  trufil  17943  alexsubALT  18083  cnextcn  18099  ucnima  18312  iducn  18314  bl2in  18431  addcnlem  18895  rescncf  18928  ovoliunlem2  19400  voliun  19449  mbflimsup  19559  itgcn  19735  dvdsq1p  20084  aalioulem2  20251  recosf1o  20438  logrec  20662  xrlimcnp  20808  basellem4  20867  bposlem1  21069  bposlem5  21073  lgsdchrval  21132  pntlem3  21304  usgraedgprv  21397  usgraedgrnv  21398  usgrafisinds  21428  eupai  21690  elghomlem2  21951  blocn2  22310  htthlem  22421  axhcompl-zf  22502  spanuni  23047  spansncol  23071  spansneleq  23073  elspansn5  23077  idcnop  23485  pjnormssi  23672  dmdmd  23804  bian1d  23951  ifeqeqx  24002  supxrnemnf  24128  rexdiv  24173  xrstos  24202  cnre2csqlem  24309  lmxrge0  24338  qqhval2lem  24366  esumpr2  24459  esumcvg  24477  issgon  24507  measxun2  24565  measres  24577  measdivcstOLD  24579  measdivcst  24580  elorrvc  24722  erdsze2lem2  24891  cvmsval  24954  ghomgsg  25105  ghomf1olem  25106  dedekindle  25189  fprod2dlem  25305  fundmpss  25391  dfon2lem3  25413  frmin  25518  poseq  25529  soseq  25530  wfrlem5  25543  wfrlem12  25550  frrlem5  25587  frrlem11  25595  nobndup  25656  nobnddown  25657  dfrdg4  25796  brbtwn2  25845  axbtwnid  25879  cgrtriv  25937  btwntriv2  25947  ifscgr  25979  lineext  26011  btwnconn1lem12  26033  colinbtwnle  26053  ontgval  26182  onsucconi  26188  ltflcei  26240  itg2addnclem  26257  areacirclem2  26294  areacirclem5  26297  areacirc  26298  elicc3  26321  comppfsc  26388  nninfnub  26456  prdstotbnd  26504  heiborlem4  26524  heibor  26531  grpokerinj  26561  isidlc  26626  prtlem17  26726  elrfirn2  26751  rencldnfilem  26882  sdrgacs  27487  stoweidlem35  27761  stoweidlem48  27774  rexrsb  27924  funbrafv  27999  rlimdmafv  28018  fzoopth  28140  2ffzoeq  28141  swrd0  28184  swrdccatin12lem3  28213  swrdccat  28217  swrdccat3blem  28219  prmgt1  28224  2cshw2lem2  28254  iswlkg  28301  snelpwrVD  28944  en3lplem1VD  28956  en3lpVD  28958  orbi1rVD  28961  sbc3orgVD  28964  3impexpVD  28969  equncomVD  28981  trsbcVD  28990  trintALTVD  28993  trintALT  28994  csbingVD  28997  csbsngVD  29006  csbxpgVD  29007  csbrngVD  29009  csbfv12gALTVD  29012  relopabVD  29014  e2ebindVD  29025  bnj580  29285  ax10lem4NEW7  29472  dral1NEW7  29494  cbvalwwAUX7  29520  ax16iNEW7  29552  sbequiNEW7  29580  speivNEW7  29626  ax7w6AUX7  29653  cbvalOLD7  29726  a16gALTOLD7  29745  sb9iOLD7  29759  lsator0sp  29800  atlrelat1  30120  cvratlem  30219  diaintclN  31857  dibintclN  31966  cdlemn11pre  32009  dihord2pre  32024  dihintcl  32143  dochkrshp4  32188  lcfrlem9  32349  lcfrlem21  32362  mapdh8e  32583
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 179
  Copyright terms: Public domain W3C validator