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

Theorem biimprd 214
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 19 . 2  |-  ( ch 
->  ch )
2 biimprd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibr 212 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  syl6bir  220  mpbird  223  sylibrd  225  sylbird  226  con4bid  284  mtbid  291  mtbii  293  imbi1d  308  biimpar  471  prlem1  928  spfw  1657  spw  1660  cbvalw  1675  cbvalvw  1676  alcomiw  1678  ax10lem2  1877  ax10lem4  1881  dral1  1905  cbval  1924  speiv  1940  ax16i  1986  a16gALT  1989  sbequi  1999  sb9i  2034  dral1-o  2093  a16g-o  2125  cleqh  2380  pm13.18  2518  rspcimdv  2885  rspcedv  2888  moi2  2946  moi  2948  sspsstr  3281  isso2i  4346  wefrc  4387  oneqmini  4443  ordsssuc2  4481  ordtri2or  4488  reusv6OLD  4545  reusv7OLD  4546  ralxfrd  4548  ralxfr2d  4550  orduniorsuc  4621  ordzsl  4636  tfinds  4650  elres  4990  sotri3  5073  2elresin  5355  f1ocnv  5485  tz6.12c  5547  fveqres  5560  fvun1  5590  dffo4  5676  fconst5  5731  isores3  5832  f1owe  5850  f1oweALT  5851  weniso  5852  ndmovordi  6011  fnse  6232  tposfo2  6257  issmo2  6366  iordsmo  6374  smoel2  6380  tz7.48lem  6453  abianfp  6471  oawordeulem  6552  om00  6573  omlimcl  6576  odi  6577  nnawordi  6619  fiint  7133  fipreima  7161  dffi2  7176  suplub2  7212  wemapso2lem  7265  unwdomg  7298  inf3lem3  7331  trcl  7410  fidomtri  7626  prdom2  7636  cardaleph  7716  ackbij1lem16  7861  coflim  7887  coftr  7899  infpssrlem4  7932  isfin7-2  8022  axdc3lem2  8077  axdc3lem4  8079  brdom6disj  8157  entric  8179  fpwwe2lem12  8263  inatsk  8400  grur1a  8441  indpi  8531  reclem3pr  8673  supsrlem  8733  lelttr  8912  fimaxre  9701  nnmulcl  9769  arch  9962  nnnegz  10027  zeo  10097  uzm1  10258  negn0  10304  rpneg  10383  xrlttri  10473  xrlelttr  10487  iccid  10701  icoshft  10758  fzen  10811  elfz2nn0  10821  fzm1  10862  max0add  11795  abslt  11798  absle  11799  rexuzre  11836  caurcvg  12149  caucvg  12151  dvdsval2  12534  negdvdsb  12545  muldvds2  12554  smuval2  12673  smupvallem  12674  rplpwr  12735  alginv  12745  algfx  12750  rpexp1i  12800  qnumdencl  12810  phiprmpw  12844  prmdiveq  12854  pcmpt  12940  infpnlem1  12957  imasaddfnlem  13430  plelttr  14106  lubid  14116  mndodconglem  14856  cnpnei  16993  uncon  17155  kqsat  17422  isr0  17428  qtophmeo  17508  trufil  17605  alexsubALT  17745  bl2in  17957  addcnlem  18368  rescncf  18401  ovoliunlem2  18862  voliun  18911  mbflimsup  19021  itgcn  19197  dvdsq1p  19546  aalioulem2  19713  recosf1o  19897  logrec  20117  xrlimcnp  20263  basellem4  20321  bposlem1  20523  bposlem5  20527  lgsdchrval  20586  pntlem3  20758  elghomlem2  21029  blocn2  21386  htthlem  21497  axhcompl-zf  21578  spanuni  22123  spansncol  22147  spansneleq  22149  elspansn5  22153  idcnop  22561  pjnormssi  22748  dmdmd  22880  ifeqeqx  23034  rexdiv  23109  bian1d  23122  eqrd  23126  rnmpt2ss  23239  supxrnemnf  23256  iocinif  23274  unitdivcld  23285  cnre2csqlem  23294  tpr2rico  23296  lmxrge0  23375  esumpr2  23439  esumcvg  23454  issgon  23484  measxun2  23538  measres  23549  measdivcstOLD  23551  measdivcst  23552  imambfm  23567  cnmbfm  23568  mbfmco2  23570  elorrvc  23664  erdsze2lem2  23735  cvmsval  23797  eupai  23883  ghomgsg  24000  ghomf1olem  24001  dedekindle  24083  fundmpss  24122  dfon2lem3  24141  frmin  24242  poseq  24253  soseq  24254  wfrlem5  24260  wfrlem10  24265  wfrlem12  24267  frrlem5  24285  frrlem11  24293  nobndup  24354  nobnddown  24355  dfrdg4  24488  brbtwn2  24533  axbtwnid  24567  cgrtriv  24625  btwntriv2  24635  ifscgr  24667  lineext  24699  btwnconn1lem12  24721  colinbtwnle  24741  ontgval  24870  onsucconi  24876  areacirclem4  24927  areacirclem6  24930  areacirc  24931  boxbid  25011  nxtbid  25012  diabid  25013  untbi12d  25022  repfuntw  25160  cbicp  25166  prodeq3ii  25308  dffprod  25319  ablocomgrp  25342  abhp  26173  elicc3  26228  comppfsc  26307  nninfnub  26461  prdstotbnd  26518  heiborlem4  26538  heibor  26545  grpokerinj  26575  isidlc  26640  prtlem17  26744  elrfirn2  26771  rencldnfilem  26903  sdrgacs  27509  stoweidlem18  27767  stoweidlem27  27776  stoweidlem35  27784  stoweidlem48  27797  rexrsb  27947  funbrafv  28020  usgraedgprv  28122  usgraedgrnv  28123  snelpwrVD  28606  en3lplem1VD  28619  en3lpVD  28621  orbi1rVD  28624  sbc3orgVD  28627  3impexpVD  28632  equncomVD  28644  trsbcVD  28653  trintALTVD  28656  trintALT  28657  csbingVD  28660  csbsngVD  28669  csbxpgVD  28670  csbrngVD  28672  csbfv12gALTVD  28675  relopabVD  28677  e2ebindVD  28688  bnj580  28945  ax10lem18ALT  29124  lsator0sp  29191  atlrelat1  29511  cvratlem  29610  diaintclN  31248  dibintclN  31357  cdlemn11pre  31400  dihord2pre  31415  dihintcl  31534  dochkrshp4  31579  lcfrlem9  31740  lcfrlem21  31753  mapdh8e  31974
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 177
  Copyright terms: Public domain W3C validator