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, 11-Jan-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  485  prlem1  953  spfw  1744  cbvalw  1746  alcomiw  1749  nfimd  1850  cbval  1969  axc11nlem  1996  axc16i  2012  equvini  2037  axc16gALT  2056  sbequi  2066  sb9iOLD  2128  dral1-o  2204  ax16g-o  2235  cleqhOLD  2543  pm13.18  2688  rspcimdv  3079  rspcedv  3082  moi2  3145  moi  3147  eqrd  3379  sspsstr  3466  reusv6OLD  4508  reusv7OLD  4509  ralxfrd  4511  ralxfr2d  4513  isso2i  4678  wefrc  4719  oneqmini  4775  ordsssuc2  4812  ordtri2or  4819  elres  5150  sotri3  5233  2elresin  5527  f1ocnv  5658  tz6.12c  5714  fveqres  5729  fvun1  5767  dffo4  5864  fconst5  5940  fnprb  5941  fnprOLD  5942  isores3  6031  f1owe  6049  weniso  6050  ndmovordi  6259  orduniorsuc  6446  ordzsl  6461  tfinds  6475  f1oweALT  6566  fnse  6694  tposfo2  6773  issmo2  6815  iordsmo  6823  smoel2  6829  tz7.48lem  6901  oawordeulem  6998  om00  7019  omlimcl  7022  odi  7023  nnawordi  7065  fiint  7593  fipreima  7622  dffi2  7678  suplub2  7716  wemapsolem  7769  unwdomg  7804  inf3lem3  7841  trcl  7953  fidomtri  8168  prdom2  8178  cardaleph  8264  ackbij1lem16  8409  coflim  8435  coftr  8447  infpssrlem4  8480  isfin7-2  8570  axdc3lem2  8625  axdc3lem4  8627  brdom6disj  8704  entric  8726  fpwwe2lem12  8813  inatsk  8950  grur1a  8991  indpi  9081  reclem3pr  9223  supsrlem  9283  lelttr  9470  dedekindle  9539  fimaxre  10282  nnmulcl  10350  arch  10581  nnnegz  10654  zeo  10732  uzm1  10896  negn0  10946  rpneg  11025  xrlttri  11121  xrlelttr  11135  iccid  11350  icoshft  11412  fzen  11472  elfz2nn0  11485  fzm1  11545  fleqceilz  11698  zmodidfzoimp  11743  hasheqf1oi  12127  hashnfinnn0  12135  swrd0  12332  swrdccatin12lem2  12385  swrdccat  12389  swrdccat3blem  12391  repswswrd  12427  max0add  12804  abslt  12807  absle  12808  rexuzre  12845  caurcvg  13159  caucvg  13161  dvdsval2  13543  negdvdsb  13554  muldvds2  13563  smuval2  13683  smupvallem  13684  rplpwr  13745  alginv  13755  algfx  13760  prmgt1  13787  rpexp1i  13812  qnumdencl  13822  phiprmpw  13856  prmdiveq  13866  pcmpt  13959  infpnlem1  13976  imasaddfnlem  14471  plelttr  15147  lubval  15159  lublecllem  15163  glbval  15172  mrcmndind  15499  mndodconglem  16049  elfrlmbasn0  18195  mavmulsolcl  18367  slesolex  18493  cnpnei  18873  uncon  19038  kqsat  19309  isr0  19315  qtophmeo  19395  trufil  19488  alexsubALT  19628  cnextcn  19644  ucnima  19861  iducn  19863  bl2in  19980  addcnlem  20445  rescncf  20478  ovoliunlem2  20991  voliun  21040  mbflimsup  21149  itgcn  21325  dvdsq1p  21637  aalioulem2  21804  recosf1o  21996  logrec  22220  xrlimcnp  22367  basellem4  22426  bposlem1  22628  bposlem5  22632  lgsdchrval  22691  pntlem3  22863  brbtwn2  23156  axbtwnid  23190  usgraedgprv  23300  usgraedgrnv  23301  usgrafisinds  23331  eupai  23593  elghomlem2  23854  blocn2  24213  htthlem  24324  axhcompl-zf  24405  spanuni  24952  spansncol  24976  spansneleq  24978  elspansn5  24982  idcnop  25390  pjnormssi  25577  dmdmd  25709  bian1d  25856  ifeqeqx  25907  supxrnemnf  26061  rexdiv  26106  xrstos  26145  xrge0omnd  26179  cnre2csqlem  26345  fsumcvg4  26385  lmxrge0  26387  qqhval2lem  26415  esumpr2  26522  esumcvg  26540  issgon  26571  measxun2  26629  measres  26641  measdivcstOLD  26643  measdivcst  26644  elorrvc  26851  signsply0  26957  erdsze2lem2  27097  cvmsval  27160  ghomgsg  27317  ghomf1olem  27318  fprod2dlem  27496  fundmpss  27582  dfon2lem3  27603  frmin  27708  poseq  27719  soseq  27720  wfrlem5  27733  wfrlem12  27740  frrlem5  27777  frrlem11  27785  nobndup  27846  nobnddown  27847  dfrdg4  27986  cgrtriv  28038  btwntriv2  28048  ifscgr  28080  lineext  28112  btwnconn1lem12  28134  colinbtwnle  28154  ontgval  28282  onsucconi  28288  wl-nfs1t  28372  finixpnum  28419  ltflcei  28424  itg2addnclem  28448  areacirclem2  28490  areacirclem5  28493  areacirc  28494  elicc3  28517  comppfsc  28584  nninfnub  28652  prdstotbnd  28698  heiborlem4  28718  heibor  28725  grpokerinj  28755  isidlc  28820  prtlem17  29026  elrfirn2  29037  rencldnfilem  29164  sdrgacs  29563  stoweidlem35  29835  stoweidlem48  29848  rexrsb  29998  funbrafv  30069  rlimdmafv  30088  fzoopth  30218  2ffzoeq  30219  elfzom1p1elfzo  30220  iswlkg  30290  isclwlkg  30425  clwlkisclwwlklem2a1  30446  clwwisshclww  30476  clwlksizeeq  30530  numclwwlkovf2ex  30684  numclwwlk2lem1  30700  numclwwlk5lem  30709  frgrareggt1  30714  friendship  30720  ellcoellss  30974  snelpwrVD  31572  en3lplem1VD  31584  en3lpVD  31586  orbi1rVD  31589  sbc3orgVD  31592  3impexpVD  31597  equncomVD  31609  trsbcVD  31618  trintALTVD  31621  trintALT  31622  csbingVD  31625  csbsngVD  31634  csbxpgVD  31635  csbrngVD  31637  csbfv12gALTVD  31640  relopabVD  31642  e2ebindVD  31653  bnj580  31911  bj-bibibi  32117  bj-cbvalv  32237  bj-axc11nlemv  32255  bj-cleqh  32298  bj-equsal  32339  bj-finsumval0  32588  lsator0sp  32651  atlrelat1  32971  cvratlem  33070  diaintclN  34708  dibintclN  34817  cdlemn11pre  34860  dihord2pre  34875  dihintcl  34994  dochkrshp4  35039  lcfrlem9  35200  lcfrlem21  35213  mapdh8e  35434
  Copyright terms: Public domain W3C validator