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  1682  spw  1685  cbvalw  1692  cbvalvw  1693  alcomiw  1695  nfimd  1786  ax10lem2  1909  ax10lem4  1913  dral1  1937  cbval  1956  speiv  1972  ax16i  2018  a16gALT  2021  sbequi  2031  sb9i  2066  dral1-o  2126  a16g-o  2158  cleqh  2413  pm13.18  2551  rspcimdv  2919  rspcedv  2922  moi2  2980  moi  2982  sspsstr  3315  isso2i  4383  wefrc  4424  oneqmini  4480  ordsssuc2  4518  ordtri2or  4525  reusv6OLD  4582  reusv7OLD  4583  ralxfrd  4585  ralxfr2d  4587  orduniorsuc  4658  ordzsl  4673  tfinds  4687  elres  5027  sotri3  5110  2elresin  5392  f1ocnv  5523  tz6.12c  5585  fveqres  5598  fvun1  5628  dffo4  5714  fconst5  5770  fnpr  5771  fnprOLD  5772  isores3  5874  f1owe  5892  f1oweALT  5893  weniso  5894  ndmovordi  6053  fnse  6274  tposfo2  6299  issmo2  6408  iordsmo  6416  smoel2  6422  tz7.48lem  6495  abianfp  6513  oawordeulem  6594  om00  6615  omlimcl  6618  odi  6619  nnawordi  6661  fiint  7178  fipreima  7206  dffi2  7221  suplub2  7257  wemapso2lem  7310  unwdomg  7343  inf3lem3  7376  trcl  7455  fidomtri  7671  prdom2  7681  cardaleph  7761  ackbij1lem16  7906  coflim  7932  coftr  7944  infpssrlem4  7977  isfin7-2  8067  axdc3lem2  8122  axdc3lem4  8124  brdom6disj  8202  entric  8224  fpwwe2lem12  8308  inatsk  8445  grur1a  8486  indpi  8576  reclem3pr  8718  supsrlem  8778  lelttr  8957  fimaxre  9746  nnmulcl  9814  arch  10009  nnnegz  10074  zeo  10144  uzm1  10305  negn0  10351  rpneg  10430  xrlttri  10520  xrlelttr  10534  iccid  10748  icoshft  10805  fzen  10858  elfz2nn0  10868  fzm1  10909  max0add  11842  abslt  11845  absle  11846  rexuzre  11883  caurcvg  12196  caucvg  12198  dvdsval2  12581  negdvdsb  12592  muldvds2  12601  smuval2  12720  smupvallem  12721  rplpwr  12782  alginv  12792  algfx  12797  rpexp1i  12847  qnumdencl  12857  phiprmpw  12891  prmdiveq  12901  pcmpt  12987  infpnlem1  13004  imasaddfnlem  13479  plelttr  14155  lubid  14165  mndodconglem  14905  cnpnei  17049  uncon  17211  kqsat  17478  isr0  17484  qtophmeo  17564  trufil  17657  alexsubALT  17797  bl2in  18009  addcnlem  18420  rescncf  18453  ovoliunlem2  18915  voliun  18964  mbflimsup  19074  itgcn  19250  dvdsq1p  19599  aalioulem2  19766  recosf1o  19950  logrec  20170  xrlimcnp  20316  basellem4  20374  bposlem1  20576  bposlem5  20580  lgsdchrval  20639  pntlem3  20811  elghomlem2  21082  blocn2  21441  htthlem  21552  axhcompl-zf  21633  spanuni  22178  spansncol  22202  spansneleq  22204  elspansn5  22208  idcnop  22616  pjnormssi  22803  dmdmd  22935  bian1d  23084  eqrd  23132  ifeqeqx  23144  rnmpt2ss  23236  supxrnemnf  23273  iocinif  23291  rexdiv  23324  unitdivcld  23368  cnre2csqlem  23377  tpr2rico  23379  lmxrge0  23406  ucnima  23474  iducn  23476  qqhval2lem  23560  esumpr2  23634  esumcvg  23652  issgon  23682  measxun2  23738  measres  23750  measdivcstOLD  23752  measdivcst  23753  imambfm  23786  cnmbfm  23787  mbfmco2  23789  elorrvc  23895  erdsze2lem2  24019  cvmsval  24081  eupai  24167  ghomgsg  24284  ghomf1olem  24285  dedekindle  24369  fundmpss  24507  dfon2lem3  24526  frmin  24627  poseq  24638  soseq  24639  wfrlem5  24645  wfrlem10  24650  wfrlem12  24652  frrlem5  24670  frrlem11  24678  nobndup  24739  nobnddown  24740  dfrdg4  24874  brbtwn2  24919  axbtwnid  24953  cgrtriv  25011  btwntriv2  25021  ifscgr  25053  lineext  25085  btwnconn1lem12  25107  colinbtwnle  25127  ontgval  25256  onsucconi  25262  ltflcei  25312  itg2addnclem  25317  areacirclem4  25344  areacirclem6  25347  areacirc  25348  elicc3  25377  comppfsc  25456  nninfnub  25610  prdstotbnd  25666  heiborlem4  25686  heibor  25693  grpokerinj  25723  isidlc  25788  prtlem17  25892  elrfirn2  25919  rencldnfilem  26051  sdrgacs  26657  stoweidlem18  26915  stoweidlem27  26924  stoweidlem35  26932  stoweidlem48  26945  rexrsb  27095  funbrafv  27171  rlimdmafv  27190  hasheqf1oi  27290  usgraedgprv  27348  usgraedgrnv  27349  snelpwrVD  28117  en3lplem1VD  28130  en3lpVD  28132  orbi1rVD  28135  sbc3orgVD  28138  3impexpVD  28143  equncomVD  28155  trsbcVD  28164  trintALTVD  28167  trintALT  28168  csbingVD  28171  csbsngVD  28180  csbxpgVD  28181  csbrngVD  28183  csbfv12gALTVD  28186  relopabVD  28188  e2ebindVD  28199  bnj580  28456  ax10lem4NEW7  28643  dral1NEW7  28665  cbvalwwAUX7  28689  ax16iNEW7  28721  sbequiNEW7  28748  speivNEW7  28792  ax7w6AUX7  28818  cbvalOLD7  28875  a16gALTOLD7  28894  sb9iOLD7  28908  ax10lem18ALT  28942  lsator0sp  29009  atlrelat1  29329  cvratlem  29428  diaintclN  31066  dibintclN  31175  cdlemn11pre  31218  dihord2pre  31233  dihintcl  31352  dochkrshp4  31397  lcfrlem9  31558  lcfrlem21  31571  mapdh8e  31792
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