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  960  spfw  1790  cbvalw  1792  alcomiw  1795  ax12v  1839  nfimd  1901  axc11nlem  1922  cbval  2005  axc11nlemOLD  2032  axc16i  2048  equvini  2071  axc16gALT  2090  sbequi  2100  dral1-o  2217  ax16g-o  2248  eqrdav  2439  cleqhOLD  2557  pm13.18  2752  rspcimdv  3195  rspcedv  3198  moi2  3264  moi  3266  eqrd  3504  sspsstr  3591  reusv6OLD  4644  reusv7OLD  4645  ralxfrd  4647  ralxfr2d  4649  isso2i  4818  wefrc  4859  oneqmini  4915  ordsssuc2  4952  ordtri2or  4959  elres  5295  sotri3  5383  2elresin  5678  f1ocnv  5814  tz6.12c  5871  fveqres  5886  fvun1  5925  dffo4  6028  fconst5  6109  fnprb  6110  fnprOLD  6111  isores3  6212  f1owe  6230  weniso  6231  ndmovordi  6447  orduniorsuc  6646  ordzsl  6661  tfinds  6675  f1oweALT  6765  fnse  6898  tposfo2  6976  issmo2  7018  iordsmo  7026  smoel2  7032  tz7.48lem  7104  oawordeulem  7201  om00  7222  omlimcl  7225  odi  7226  nnawordi  7268  fiint  7795  fipreima  7824  dffi2  7881  suplub2  7919  wemapsolem  7973  unwdomg  8008  inf3lem3  8045  trcl  8157  fidomtri  8372  prdom2  8382  cardaleph  8468  ackbij1lem16  8613  coflim  8639  coftr  8651  infpssrlem4  8684  isfin7-2  8774  axdc3lem2  8829  axdc3lem4  8831  brdom6disj  8908  entric  8930  fpwwe2lem12  9017  inatsk  9154  grur1a  9195  indpi  9283  reclem3pr  9425  supsrlem  9486  lelttr  9673  dedekindle  9743  fimaxre  10491  nnmulcl  10560  arch  10793  nnnegz  10868  zeo  10949  uzm1  11115  negn0  11172  rpneg  11253  xrlttri  11349  xrlelttr  11363  iccid  11578  icoshft  11646  fzen  11707  fzm1  11762  elfz2nn0  11772  elfzom1p1elfzo  11869  fleqceilz  11955  zmodidfzoimp  12000  hasheqf1oi  12398  hashnfinnn0  12406  swrd0  12632  swrdccatin12lem2  12688  swrdccat  12692  swrdccat3blem  12694  repswswrd  12730  max0add  13117  abslt  13121  absle  13122  rexuzre  13159  caurcvg  13473  caucvg  13475  dvdsval2  13861  negdvdsb  13872  muldvds2  13881  smuval2  14004  smupvallem  14005  rplpwr  14066  alginv  14076  algfx  14081  prmgt1  14108  rpexp1i  14134  qnumdencl  14144  phiprmpw  14178  prmdiveq  14188  pcmpt  14283  infpnlem1  14300  imasaddfnlem  14797  plelttr  15471  lubval  15483  lublecllem  15487  glbval  15496  mrcmndind  15866  mndodconglem  16434  elfrlmbasn0  18663  mavmulsolcl  18920  slesolex  19051  fvmptnn04if  19217  chfacfisf  19222  chfacfisfcpmat  19223  cnpnei  19631  uncon  19796  comppfsc  19899  kqsat  20098  isr0  20104  qtophmeo  20184  trufil  20277  alexsubALT  20417  cnextcn  20433  ucnima  20650  iducn  20652  bl2in  20769  addcnlem  21234  rescncf  21267  ovoliunlem2  21780  voliun  21830  mbflimsup  21939  itgcn  22115  dvdsq1p  22427  aalioulem2  22594  recosf1o  22787  logrec  23016  xrlimcnp  23163  basellem4  23222  bposlem1  23424  bposlem5  23428  lgsdchrval  23487  pntlem3  23659  brbtwn2  24073  axbtwnid  24107  usgraedgprv  24241  usgraedgrnv  24242  usgrafisinds  24278  iswlkg  24389  isclwlkg  24620  clwlkisclwwlklem2a1  24644  clwwisshclww  24672  clwlksizeeq  24717  eupai  24832  numclwwlkovf2ex  24951  numclwwlk2lem1  24967  numclwwlk5lem  24976  frgrareggt1  24981  friendship  24987  elghomlem2OLD  25229  blocn2  25588  htthlem  25699  axhcompl-zf  25780  spanuni  26327  spansncol  26351  spansneleq  26353  elspansn5  26357  idcnop  26765  pjnormssi  26952  dmdmd  27084  bian1d  27231  ifeqeqx  27284  supxrnemnf  27448  rexdiv  27488  xrstos  27533  xrge0omnd  27567  cnre2csqlem  27758  fsumcvg4  27798  lmxrge0  27800  qqhval2lem  27828  esumpr2  27940  esumcvg  27958  issgon  27989  measxun2  28047  measres  28059  measdivcstOLD  28061  measdivcst  28062  elorrvc  28268  signsply0  28374  erdsze2lem2  28514  cvmsval  28577  ghomgsg  28899  ghomf1olem  28900  fundmpss  29164  dfon2lem3  29185  frmin  29290  poseq  29301  soseq  29302  wfrlem5  29315  wfrlem12  29322  frrlem5  29359  frrlem11  29367  nobndup  29428  nobnddown  29429  dfrdg4  29568  cgrtriv  29620  btwntriv2  29630  ifscgr  29662  lineext  29694  btwnconn1lem12  29716  colinbtwnle  29736  ontgval  29864  onsucconi  29870  wl-nfs1t  29959  finixpnum  30006  ltflcei  30011  itg2addnclem  30034  areacirclem2  30076  areacirclem5  30079  areacirc  30080  elicc3  30103  nninfnub  30212  prdstotbnd  30258  heiborlem4  30278  heibor  30285  grpokerinj  30315  isidlc  30380  prtlem17  30585  elrfirn2  30596  rencldnfilem  30722  sdrgacs  31119  stoweidlem35  31702  stoweidlem48  31715  rexrsb  32008  funbrafv  32077  rlimdmafv  32096  fzoopth  32174  2ffzoeq  32175  usgedgvadf1lem2  32248  usgedgvadf1ALTlem2  32251  usgfis  32280  usgfisALT  32284  usgrafiedgALT  32285  mgm2mgm  32384  2zrngnmlid  32455  2zrngnmrid  32456  ellcoellss  32746  snelpwrVD  33339  en3lplem1VD  33351  en3lpVD  33353  orbi1rVD  33356  sbc3orgVD  33359  3impexpVD  33364  equncomVD  33376  trsbcVD  33385  trintALTVD  33388  trintALT  33389  csbingVD  33392  csbsngVD  33401  csbxpgVD  33402  csbrngVD  33404  csbfv12gALTVD  33407  relopabVD  33409  e2ebindVD  33420  bnj580  33678  bj-bibibi  33889  bj-cbvexw  33949  bj-cbvalv  34010  bj-axc11nlemv  34027  bj-cleqh  34070  bj-equsal  34111  bj-elid  34303  bj-finsumval0  34365  lsator0sp  34428  atlrelat1  34748  cvratlem  34847  diaintclN  36487  dibintclN  36596  cdlemn11pre  36639  dihord2pre  36654  dihintcl  36773  dochkrshp4  36818  lcfrlem9  36979  lcfrlem21  36992  mapdh8e  37213
  Copyright terms: Public domain W3C validator