MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimprd 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
Assertion
Ref Expression
biimprd

Proof of Theorem biimprd
StepHypRef Expression
1 id 22 . 2
2 biimprd.1 . 2
31, 2syl5ibr 221 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  syl6bir  229  mpbird  232  sylibrd  234  sylbird  235  con4bid  293  mtbid  300  mtbii  302  imbi1d  317  biimpar  485  prlem1  962  spfw  1806  cbvalw  1808  alcomiw  1811  ax12v  1855  nfimd  1917  axc11nlem  1938  cbval  2021  axc11nlemOLD  2048  axc16i  2064  equvini  2087  axc16gALT  2106  sbequi  2116  dral1-o  2233  ax16g-o  2264  eqrdav  2455  cleqhOLD  2573  pm13.18  2768  rspcimdv  3211  rspcedv  3214  moi2  3280  moi  3282  eqrd  3521  sspsstr  3608  reusv6OLD  4663  reusv7OLD  4664  ralxfrd  4666  ralxfr2d  4668  isso2i  4837  wefrc  4878  oneqmini  4934  ordsssuc2  4971  ordtri2or  4978  elres  5314  sotri3  5402  2elresin  5697  f1ocnv  5833  tz6.12c  5890  fveqres  5905  fvun1  5944  dffo4  6047  fconst5  6128  fnprb  6129  fnprOLD  6130  isores3  6231  f1owe  6249  weniso  6250  ndmovordi  6466  orduniorsuc  6665  ordzsl  6680  tfinds  6694  f1oweALT  6784  fnse  6917  tposfo2  6997  issmo2  7039  iordsmo  7047  smoel2  7053  tz7.48lem  7125  oawordeulem  7222  om00  7243  omlimcl  7246  odi  7247  nnawordi  7289  fiint  7817  fipreima  7846  dffi2  7903  suplub2  7941  wemapsolem  7996  unwdomg  8031  inf3lem3  8068  trcl  8180  fidomtri  8395  prdom2  8405  cardaleph  8491  ackbij1lem16  8636  coflim  8662  coftr  8674  infpssrlem4  8707  isfin7-2  8797  axdc3lem2  8852  axdc3lem4  8854  brdom6disj  8931  entric  8953  fpwwe2lem12  9040  inatsk  9177  grur1a  9218  indpi  9306  reclem3pr  9448  supsrlem  9509  lelttr  9696  dedekindle  9766  fimaxre  10515  nnmulcl  10584  arch  10817  nnnegz  10892  zeo  10973  uzm1  11140  negn0  11197  rpneg  11278  xrlttri  11374  xrlelttr  11388  iccid  11603  icoshft  11671  fzen  11732  elfz2nn0  11798  elfzom1p1elfzo  11895  fleqceilz  11981  zmodidfzoimp  12026  hasheqf1oi  12424  hashnfinnn0  12432  swrd0  12658  swrdccatin12lem2  12714  swrdccat  12718  swrdccat3blem  12720  repswswrd  12756  max0add  13143  abslt  13147  absle  13148  rexuzre  13185  caurcvg  13499  caucvg  13501  dvdsval2  13989  negdvdsb  14000  muldvds2  14009  smuval2  14132  smupvallem  14133  rplpwr  14194  alginv  14204  algfx  14209  prmgt1  14236  rpexp1i  14262  qnumdencl  14272  phiprmpw  14306  prmdiveq  14316  pcmpt  14411  infpnlem1  14428  imasaddfnlem  14925  plelttr  15602  lubval  15614  lublecllem  15618  glbval  15627  mrcmndind  15997  mndodconglem  16565  elfrlmbasn0  18796  mavmulsolcl  19053  slesolex  19184  fvmptnn04if  19350  chfacfisf  19355  chfacfisfcpmat  19356  cnpnei  19765  uncon  19930  comppfsc  20033  kqsat  20232  isr0  20238  qtophmeo  20318  trufil  20411  alexsubALT  20551  cnextcn  20567  ucnima  20784  iducn  20786  bl2in  20903  addcnlem  21368  rescncf  21401  ovoliunlem2  21914  voliun  21964  mbflimsup  22073  itgcn  22249  dvdsq1p  22561  aalioulem2  22729  recosf1o  22922  logrec  23151  xrlimcnp  23298  basellem4  23357  bposlem1  23559  bposlem5  23563  lgsdchrval  23622  pntlem3  23794  brbtwn2  24208  axbtwnid  24242  usgraedgprv  24376  usgraedgrnv  24377  usgrafisinds  24413  iswlkg  24524  isclwlkg  24755  clwlkisclwwlklem2a1  24779  clwwisshclww  24807  clwlksizeeq  24852  eupai  24967  numclwwlkovf2ex  25086  numclwwlk2lem1  25102  numclwwlk5lem  25111  frgrareggt1  25116  friendship  25122  elghomlem2OLD  25364  blocn2  25723  htthlem  25834  axhcompl-zf  25915  spanuni  26462  spansncol  26486  spansneleq  26488  elspansn5  26492  idcnop  26900  pjnormssi  27087  dmdmd  27219  bian1d  27366  ifeqeqx  27419  supxrnemnf  27583  rexdiv  27622  xrstos  27667  xrge0omnd  27701  cnre2csqlem  27892  fsumcvg4  27932  lmxrge0  27934  qqhval2lem  27962  esumpr2  28074  esumcvg  28092  issgon  28123  measxun2  28181  measres  28193  measdivcstOLD  28195  measdivcst  28196  elorrvc  28402  signsply0  28508  erdsze2lem2  28648  cvmsval  28711  ghomgsg  29033  ghomf1olem  29034  fundmpss  29196  dfon2lem3  29217  frmin  29322  poseq  29333  soseq  29334  wfrlem5  29347  wfrlem12  29354  frrlem5  29391  frrlem11  29399  nobndup  29460  nobnddown  29461  dfrdg4  29600  cgrtriv  29652  btwntriv2  29662  ifscgr  29694  lineext  29726  btwnconn1lem12  29748  colinbtwnle  29768  ontgval  29896  onsucconi  29902  wl-nfs1t  29991  finixpnum  30038  ltflcei  30043  itg2addnclem  30066  areacirclem2  30108  areacirclem5  30111  areacirc  30112  elicc3  30135  nninfnub  30244  prdstotbnd  30290  heiborlem4  30310  heibor  30317  grpokerinj  30347  isidlc  30412  prtlem17  30617  elrfirn2  30628  rencldnfilem  30754  sdrgacs  31150  stoweidlem35  31817  stoweidlem48  31830  rexrsb  32174  funbrafv  32243  rlimdmafv  32262  fzoopth  32340  2ffzoeq  32341  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  usgfis  32446  usgfisALT  32450  usgrafiedgALT  32451  mgm2mgm  32551  2zrngnmlid  32755  2zrngnmrid  32756  ellcoellss  33036  snelpwrVD  33631  en3lplem1VD  33643  en3lpVD  33645  orbi1rVD  33648  sbc3orgVD  33651  3impexpVD  33656  equncomVD  33668  trsbcVD  33677  trintALTVD  33680  trintALT  33681  csbingVD  33684  csbsngVD  33693  csbxpgVD  33694  csbrngVD  33696  csbfv12gALTVD  33699  relopabVD  33701  e2ebindVD  33712  bnj580  33971  bj-bibibi  34175  bj-cbvexw  34235  bj-cbvalv  34296  bj-axc11nlemv  34315  bj-cleqh  34358  bj-equsal  34399  bj-elid  34599  bj-finsumval0  34663  lsator0sp  34726  atlrelat1  35046  cvratlem  35145  diaintclN  36785  dibintclN  36894  cdlemn11pre  36937  dihord2pre  36952  dihintcl  37071  dochkrshp4  37116  lcfrlem9  37277  lcfrlem21  37290  mapdh8e  37511  intimasn  37771
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
  Copyright terms: Public domain W3C validator