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  1659  spw  1662  cbvalw  1677  cbvalvw  1678  alcomiw  1680  ax10lem2  1879  ax10lem4  1883  dral1  1907  cbval  1926  speiv  1942  ax16i  1988  a16gALT  1991  sbequi  2001  sb9i  2036  dral1-o  2095  a16g-o  2127  cleqh  2382  pm13.18  2520  rspcimdv  2887  rspcedv  2890  moi2  2948  moi  2950  sspsstr  3283  isso2i  4348  wefrc  4389  oneqmini  4445  ordsssuc2  4483  ordtri2or  4490  reusv6OLD  4547  reusv7OLD  4548  ralxfrd  4550  ralxfr2d  4552  orduniorsuc  4623  ordzsl  4638  tfinds  4652  elres  4992  sotri3  5075  2elresin  5357  f1ocnv  5487  tz6.12c  5549  fveqres  5562  fvun1  5592  dffo4  5678  fconst5  5733  isores3  5834  f1owe  5852  f1oweALT  5853  weniso  5854  ndmovordi  6013  fnse  6234  tposfo2  6259  issmo2  6368  iordsmo  6376  smoel2  6382  tz7.48lem  6455  abianfp  6473  oawordeulem  6554  om00  6575  omlimcl  6578  odi  6579  nnawordi  6621  fiint  7135  fipreima  7163  dffi2  7178  suplub2  7214  wemapso2lem  7267  unwdomg  7300  inf3lem3  7333  trcl  7412  fidomtri  7628  prdom2  7638  cardaleph  7718  ackbij1lem16  7863  coflim  7889  coftr  7901  infpssrlem4  7934  isfin7-2  8024  axdc3lem2  8079  axdc3lem4  8081  brdom6disj  8159  entric  8181  fpwwe2lem12  8265  inatsk  8402  grur1a  8443  indpi  8533  reclem3pr  8675  supsrlem  8735  lelttr  8914  fimaxre  9703  nnmulcl  9771  arch  9964  nnnegz  10029  zeo  10099  uzm1  10260  negn0  10306  rpneg  10385  xrlttri  10475  xrlelttr  10489  iccid  10703  icoshft  10760  fzen  10813  elfz2nn0  10823  fzm1  10864  max0add  11797  abslt  11800  absle  11801  rexuzre  11838  caurcvg  12151  caucvg  12153  dvdsval2  12536  negdvdsb  12547  muldvds2  12556  smuval2  12675  smupvallem  12676  rplpwr  12737  alginv  12747  algfx  12752  rpexp1i  12802  qnumdencl  12812  phiprmpw  12846  prmdiveq  12856  pcmpt  12942  infpnlem1  12959  imasaddfnlem  13432  plelttr  14108  lubid  14118  mndodconglem  14858  cnpnei  16995  uncon  17157  kqsat  17424  isr0  17430  qtophmeo  17510  trufil  17607  alexsubALT  17747  bl2in  17959  addcnlem  18370  rescncf  18403  ovoliunlem2  18864  voliun  18913  mbflimsup  19023  itgcn  19199  dvdsq1p  19548  aalioulem2  19715  recosf1o  19899  logrec  20119  xrlimcnp  20265  basellem4  20323  bposlem1  20525  bposlem5  20529  lgsdchrval  20588  pntlem3  20760  elghomlem2  21031  blocn2  21388  htthlem  21499  axhcompl-zf  21580  spanuni  22125  spansncol  22149  spansneleq  22151  elspansn5  22155  idcnop  22563  pjnormssi  22750  dmdmd  22882  ifeqeqx  23036  rexdiv  23111  bian1d  23124  eqrd  23128  rnmpt2ss  23241  supxrnemnf  23258  iocinif  23276  unitdivcld  23287  cnre2csqlem  23296  tpr2rico  23298  lmxrge0  23377  esumpr2  23441  esumcvg  23456  issgon  23486  measxun2  23540  measres  23551  measdivcstOLD  23553  measdivcst  23554  imambfm  23569  cnmbfm  23570  mbfmco2  23572  elorrvc  23666  erdsze2lem2  23737  cvmsval  23799  eupai  23885  ghomgsg  24002  ghomf1olem  24003  dedekindle  24085  fundmpss  24124  dfon2lem3  24143  frmin  24244  poseq  24255  soseq  24256  wfrlem5  24262  wfrlem10  24267  wfrlem12  24269  frrlem5  24287  frrlem11  24295  nobndup  24356  nobnddown  24357  dfrdg4  24490  brbtwn2  24535  axbtwnid  24569  cgrtriv  24627  btwntriv2  24637  ifscgr  24669  lineext  24701  btwnconn1lem12  24723  colinbtwnle  24743  ontgval  24872  onsucconi  24878  ltflcei  24930  itg2addnclem  24933  areacirclem4  24938  areacirclem6  24941  areacirc  24942  boxbid  25022  nxtbid  25023  diabid  25024  untbi12d  25033  repfuntw  25171  cbicp  25177  prodeq3ii  25319  dffprod  25330  ablocomgrp  25353  abhp  26184  elicc3  26239  comppfsc  26318  nninfnub  26472  prdstotbnd  26529  heiborlem4  26549  heibor  26556  grpokerinj  26586  isidlc  26651  prtlem17  26755  elrfirn2  26782  rencldnfilem  26914  sdrgacs  27520  stoweidlem18  27778  stoweidlem27  27787  stoweidlem35  27795  stoweidlem48  27808  rexrsb  27958  funbrafv  28031  usgraedgprv  28133  usgraedgrnv  28134  snelpwrVD  28679  en3lplem1VD  28692  en3lpVD  28694  orbi1rVD  28697  sbc3orgVD  28700  3impexpVD  28705  equncomVD  28717  trsbcVD  28726  trintALTVD  28729  trintALT  28730  csbingVD  28733  csbsngVD  28742  csbxpgVD  28743  csbrngVD  28745  csbfv12gALTVD  28748  relopabVD  28750  e2ebindVD  28761  bnj580  29018  ax10lem18ALT  29197  lsator0sp  29264  atlrelat1  29584  cvratlem  29683  diaintclN  31321  dibintclN  31430  cdlemn11pre  31473  dihord2pre  31488  dihintcl  31607  dochkrshp4  31652  lcfrlem9  31813  lcfrlem21  31826  mapdh8e  32047
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