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  291  mtbid  298  mtbii  300  imbi1d  315  biimpar  483  prlem1  960  spfw  1811  cbvalw  1813  alcomiw  1816  ax12v  1860  nfimd  1922  axc11nlem  1943  cbval  2026  axc11nlemOLD  2052  axc16i  2068  equvini  2091  axc16gALT  2108  sbequi  2118  dral1-o  2235  ax16g-o  2266  eqrdav  2452  cleqhOLD  2570  pm13.18  2765  rspcimdv  3208  rspcedv  3211  moi2  3277  moi  3279  eqrd  3507  sspsstr  3595  reusv6OLD  4648  reusv7OLD  4649  ralxfrd  4651  ralxfr2d  4653  isso2i  4821  wefrc  4862  oneqmini  4918  ordsssuc2  4955  ordtri2or  4962  elres  5297  sotri3  5385  2elresin  5674  f1ocnv  5810  tz6.12c  5867  fveqres  5882  fvun1  5919  dffo4  6023  fconst5  6105  fnprb  6106  isores3  6206  f1owe  6224  weniso  6225  ndmovordi  6439  orduniorsuc  6638  ordzsl  6653  tfinds  6667  f1oweALT  6757  fnse  6890  tposfo2  6970  issmo2  7012  iordsmo  7020  smoel2  7026  tz7.48lem  7098  oawordeulem  7195  om00  7216  omlimcl  7219  odi  7220  nnawordi  7262  fiint  7789  fipreima  7818  dffi2  7875  suplub2  7912  wemapsolem  7967  unwdomg  8002  inf3lem3  8038  trcl  8150  fidomtri  8365  prdom2  8375  cardaleph  8461  ackbij1lem16  8606  coflim  8632  coftr  8644  infpssrlem4  8677  isfin7-2  8767  axdc3lem2  8822  axdc3lem4  8824  brdom6disj  8901  entric  8923  fpwwe2lem12  9008  inatsk  9145  grur1a  9186  indpi  9274  reclem3pr  9416  supsrlem  9477  lelttr  9664  dedekindle  9734  fimaxre  10485  nnmulcl  10554  arch  10788  nnnegz  10863  zeo  10944  uzm1  11112  negn0  11169  rpneg  11251  xrlttri  11348  xrlelttr  11362  iccid  11577  icoshft  11645  fzen  11706  elfz2nn0  11773  elfzom1p1elfzo  11876  fleqceilz  11963  zmodidfzoimp  12009  hasheqf1oi  12409  hashnfinnn0  12417  swrd0  12653  swrdccatin12lem2  12708  swrdccat  12712  swrdccat3blem  12714  repswswrd  12750  trclublem  12916  max0add  13228  abslt  13232  absle  13233  rexuzre  13270  caurcvg  13584  caucvg  13586  dvdsval2  14076  negdvdsb  14087  muldvds2  14096  smuval2  14219  smupvallem  14220  rplpwr  14281  alginv  14291  algfx  14296  prmgt1  14323  rpexp1i  14349  qnumdencl  14359  phiprmpw  14393  prmdiveq  14403  pcmpt  14498  infpnlem1  14515  imasaddfnlem  15020  plelttr  15804  lubval  15816  lublecllem  15820  glbval  15829  mrcmndind  16199  mndodconglem  16767  elfrlmbasn0  18970  mavmulsolcl  19223  slesolex  19354  fvmptnn04if  19520  chfacfisf  19525  chfacfisfcpmat  19526  cnpnei  19935  uncon  20099  comppfsc  20202  kqsat  20401  isr0  20407  qtophmeo  20487  trufil  20580  alexsubALT  20720  cnextcn  20736  ucnima  20953  iducn  20955  bl2in  21072  addcnlem  21537  rescncf  21570  ovoliunlem2  22083  voliun  22133  mbflimsup  22242  itgcn  22418  dvdsq1p  22730  aalioulem2  22898  recosf1o  23091  logrec  23305  xrlimcnp  23499  basellem4  23558  bposlem1  23760  bposlem5  23764  lgsdchrval  23823  pntlem3  23995  brbtwn2  24413  axbtwnid  24447  usgraedgprv  24581  usgraedgrnv  24582  usgrafisinds  24618  iswlkg  24729  wwlkextinj  24935  isclwlkg  24960  clwlkisclwwlklem2a1  24984  clwwisshclww  25012  clwlksizeeq  25057  eupai  25172  numclwwlkovf2ex  25291  numclwwlk2lem1  25307  numclwwlk5lem  25316  frgrareggt1  25321  friendship  25327  elghomlem2OLD  25565  blocn2  25924  htthlem  26035  axhcompl-zf  26116  spanuni  26663  spansncol  26687  spansneleq  26689  elspansn5  26693  idcnop  27101  pjnormssi  27288  dmdmd  27420  bian1d  27567  ifeqeqx  27628  supxrnemnf  27820  rexdiv  27859  xrstos  27904  xrge0omnd  27938  cnre2csqlem  28130  fsumcvg4  28170  lmxrge0  28172  qqhval2lem  28199  esumpr2  28299  esumcvg  28318  issgon  28356  measxun2  28421  measres  28433  measdivcstOLD  28435  measdivcst  28436  elorrvc  28669  signsply0  28775  erdsze2lem2  28915  cvmsval  28978  ghomgsg  29300  ghomf1olem  29301  fundmpss  29440  dfon2lem3  29460  frmin  29565  poseq  29576  soseq  29577  wfrlem5  29590  wfrlem12  29597  frrlem5  29634  frrlem11  29642  nobndup  29703  nobnddown  29704  dfrdg4  29831  cgrtriv  29883  btwntriv2  29893  ifscgr  29925  lineext  29957  btwnconn1lem12  29979  colinbtwnle  29999  ontgval  30127  onsucconi  30133  wl-nfs1t  30234  finixpnum  30281  ltflcei  30286  itg2addnclem  30309  areacirclem2  30351  areacirclem5  30354  areacirc  30355  elicc3  30378  nninfnub  30487  prdstotbnd  30533  heiborlem4  30553  heibor  30560  grpokerinj  30590  isidlc  30655  prtlem17  30860  elrfirn2  30871  rencldnfilem  30996  sdrgacs  31394  stoweidlem35  32059  stoweidlem48  32072  rexrsb  32416  funbrafv  32485  rlimdmafv  32504  pfxccatin12lem2  32671  fzoopth  32733  2ffzoeq  32734  usgedgvadf1lem2  32805  usgedgvadf1ALTlem2  32808  usgfis  32837  usgfisALT  32841  usgrafiedgALT  32842  mgm2mgm  32942  2zrngnmlid  33028  2zrngnmrid  33029  ellcoellss  33309  nneop  33416  fldivexpfllog2  33459  digexp  33501  snelpwrVD  34050  en3lplem1VD  34062  en3lpVD  34064  orbi1rVD  34067  sbc3orgVD  34070  3impexpVD  34075  equncomVD  34088  trsbcVD  34097  trintALTVD  34100  trintALT  34101  csbingVD  34104  csbsngVD  34113  csbxpgVD  34114  csbrngVD  34116  csbfv12gALTVD  34119  relopabVD  34121  e2ebindVD  34132  bnj580  34391  bj-bibibi  34595  bj-cbvexw  34655  bj-cbvalv  34716  bj-axc11nlemv  34735  bj-cleqh  34778  bj-equsal  34819  bj-elid  35019  bj-finsumval0  35082  lsator0sp  35142  atlrelat1  35462  cvratlem  35561  diaintclN  37201  dibintclN  37310  cdlemn11pre  37353  dihord2pre  37368  dihintcl  37487  dochkrshp4  37532  lcfrlem9  37693  lcfrlem21  37706  mapdh8e  37927  intimasn  38204  ov2ssiunov2  38222  iunrelexpuztr  38227  comptiunov2i  38237
  Copyright terms: Public domain W3C validator