MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimprd Structured version   Visualization version   GIF version

Theorem biimprd 249
Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 221 and biimpri 229. (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 247 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  syl6bir  255  mpbird  258  sylibrd  260  sylbird  261  con4bid  318  mtbid  325  mtbii  327  imbi1d  343  biimpar  478  prlem1  1048  alexbii  1826  speivw  1970  spfw  2033  cbvalw  2035  alcomiw  2043  alcomiwOLD  2044  sbbidvOLD  2078  sbbidOLD  2241  cbvalv1  2355  cbval  2412  axc16i  2455  sb3  2500  sb2  2502  axc16gALT  2527  eqrdav  2825  pm13.18OLD  3103  rspcimdv  3617  rspcedv  3620  moi2  3711  moi  3713  sspsstr  4086  2nreu  4396  rabsnifsb  4657  eldifsnneqOLD  4723  ralxfr2d  5307  axprlem4  5323  sbcop1  5376  isso2i  5507  wefrc  5548  elinxp  5889  sotri3  5989  oneqmini  6241  ordsssuc2  6278  ordtri2or  6285  iotan0  6344  2elresin  6467  f1ocnv  6626  tz6.12c  6694  fveqres  6711  fvun1  6753  dffo4  6867  funopsn  6908  fconst5  6966  fnprb  6968  fntpb  6969  isores3  7082  f1owe  7100  weniso  7101  ndmovordi  7333  abnexg  7471  orduniorsuc  7538  ordzsl  7553  tfinds  7567  f1oweALT  7669  opreuopreu  7730  fnse  7823  tposfo2  7911  wfrlem5  7955  wfrlem12  7962  issmo2  7982  iordsmo  7990  smoel2  7996  tz7.48lem  8073  oawordeulem  8175  om00  8196  omlimcl  8199  odi  8200  nnawordi  8242  fiint  8789  fipreima  8824  dffi2  8881  suplub2  8919  wemapsolem  9008  unwdomg  9042  inf3lem3  9087  trcl  9164  fidomtri  9416  prdom2  9426  cardaleph  9509  ackbij1lem16  9651  coflim  9677  coftr  9689  infpssrlem4  9722  isfin7-2  9812  axdc3lem2  9867  axdc3lem4  9869  brdom6disj  9948  entric  9973  fpwwe2lem12  10057  inatsk  10194  grur1a  10235  indpi  10323  reclem3pr  10465  supsrlem  10527  lelttr  10725  dedekindle  10798  negn0  11063  fimaxre  11578  fimaxreOLD  11579  fiminre  11582  nnmulcl  11655  arch  11888  nnnegz  11978  zle0orge1  11992  zeo  12062  uzm1  12270  rpneg  12416  xrlttri  12527  xrlelttr  12544  iccid  12778  icoshft  12854  fzen  12919  elfz1b  12971  elfz2nn0  12993  fleqceilz  13217  zmodidfzoimp  13264  modsumfzodifsn  13307  hasheqf1oi  13707  hashnfinnn0  13717  hashle2prv  13831  swrd0  14015  pfxccatin12lem2  14088  swrdccat  14092  swrdccat3blem  14096  repswswrd  14141  trclublem  14350  max0add  14665  abslt  14669  absle  14670  rexuzre  14707  caurcvg  15028  caucvg  15030  dvdsval2  15605  negdvdsb  15621  muldvds2  15630  dvdsabseq  15658  smuval2  15826  smupvallem  15827  rplpwr  15902  alginv  15914  algfx  15919  coprmgcdb  15988  divgcdcoprm0  16004  oddprmgt2  16038  rpexp1i  16060  qnumdencl  16074  phiprmpw  16108  prmdiveq  16118  prm23lt5  16146  pcmpt  16223  infpnlem1  16241  prmgaplem3  16384  prmgaplem8  16389  imasaddfnlem  16796  plelttr  17577  lubval  17589  lublecllem  17593  glbval  17602  mndind  17987  mndodconglem  18605  sdrgacs  19516  elfrlmbasn0  20842  mavmulsolcl  21095  slesolex  21226  fvmptnn04if  21392  chfacfisf  21397  chfacfisfcpmat  21398  cnpnei  21807  unconn  21972  comppfsc  22075  kqsat  22274  isr0  22280  qtophmeo  22360  trufil  22453  alexsubALT  22594  cnextcn  22610  ucnima  22824  iducn  22826  bl2in  22944  addcnlem  23406  rescncf  23439  ovoliunlem2  24038  voliun  24089  mbflimsup  24201  itgcn  24377  dvdsq1p  24688  aalioulem2  24856  recosf1o  25051  logrec  25273  xrlimcnp  25479  basellem4  25594  bposlem1  25793  bposlem5  25797  lgsqrmod  25861  lgsdchrval  25863  2lgslem1a1  25898  pntlem3  26118  brbtwn2  26624  axbtwnid  26658  elntg2  26704  umgredgprv  26825  umgrpredgv  26858  usgredgprvALT  26910  fusgrfisstep  27044  fusgrfis  27045  nbupgr  27059  nbumgrvtx  27061  finsumvtxdg2size  27265  wlkp1lem8  27395  upgr2pthnlp  27446  wwlksnextinj  27610  usgr2wspthons3  27676  clwwlkccatlem  27700  clwlkclwwlklem2a1  27703  clwwisshclwws  27726  wwlksext2clwwlk  27769  clwwlknonex2lem2  27820  eucrctshift  27955  eucrct2eupth  27957  numclwwlk2lem1  28088  numclwwlk5lem  28099  frgrreggt1  28105  frgrreg  28106  friendship  28111  blocn2  28518  htthlem  28627  axhcompl-zf  28708  spanuni  29254  spansncol  29278  spansneleq  29280  elspansn5  29284  idcnop  29691  pjnormssi  29878  dmdmd  30010  bian1d  30157  ifeqeqx  30230  opabssi  30298  supxrnemnf  30425  rexdiv  30535  xrstos  30599  xrge0omnd  30645  cnre2csqlem  31058  fsumcvg4  31098  lmxrge0  31100  qqhval2lem  31127  esumpr2  31231  esumcvg  31250  issgon  31287  measxun2  31374  measres  31386  measdivcst  31388  measdivcstALTV  31389  elorrvc  31626  signsply0  31726  bnj580  32090  0nn0m1nnn0  32254  umgracycusgr  32304  erdsze2lem2  32354  cvmsval  32416  fmlasuc  32536  fundmpss  32912  dfon2lem3  32933  frmin  32987  poseq  32998  soseq  32999  fprlem1  33040  frrlem15  33045  nosupbnd1  33117  dfrdg4  33315  cgrtriv  33366  btwntriv2  33376  ifscgr  33408  lineext  33440  btwnconn1lem12  33462  colinbtwnle  33482  elicc3  33568  ontgval  33682  onsucconni  33688  bj-bibibi  33823  bj-cbval  33885  bj-cbvex  33886  bj-cbvexw  33912  bj-equsal  34052  bj-restn0  34281  bj-snmoore  34305  bj-elsn0  34345  bj-finsumval0  34461  relowlssretop  34532  sucneqond  34534  finxpsuc  34567  pibt2  34586  wl-nfs1t  34664  finixpnum  34763  ltflcei  34766  matunitlindflem1  34774  poimirlem23  34801  poimirlem24  34802  poimirlem27  34805  poimirlem32  34810  itg2addnclem  34829  areacirclem2  34869  areacirclem5  34872  areacirc  34873  nninfnub  34913  prdstotbnd  34959  heiborlem4  34979  heibor  34986  elghomlem2OLD  35051  grpokerinj  35058  isidlc  35180  prtlem17  35898  dral1-o  35926  axc16g-o  35956  lsator0sp  36023  atlrelat1  36343  cvratlem  36443  diaintclN  38080  dibintclN  38189  cdlemn11pre  38232  dihord2pre  38247  dihintcl  38366  dochkrshp4  38411  lcfrlem9  38572  lcfrlem21  38585  mapdh8e  38806  0prjspnrel  39153  elrfirn2  39177  rencldnfilem  39301  refimssco  39851  rtrclex  39861  intimasn  39886  ss2iundf  39888  ov2ssiunov2  39929  comptiunov2i  39935  iunrelexpuztr  39948  dssmapf1od  40251  mnuprdlem1  40492  mnuprdlem2  40493  snelpwrVD  41049  en3lplem1VD  41061  en3lpVD  41063  orbi1rVD  41066  sbc3orgVD  41069  3impexpVD  41074  equncomVD  41086  trsbcVD  41095  trintALTVD  41098  trintALT  41099  csbingVD  41102  csbsngVD  41111  csbxpgVD  41112  csbrngVD  41114  csbfv12gALTVD  41117  relopabVD  41119  e2ebindVD  41130  xlimpnfxnegmnf  41979  xlimbr  41992  stoweidlem35  42205  stoweidlem48  42218  rexrsb  43183  2reu8i  43197  funbrafv  43242  rlimdmafv  43261  tz6.12c-afv2  43326  rlimdmafv2  43342  fzopredsuc  43408  fzoopth  43412  2ffzoeq  43413  iccpartlt  43435  proththd  43630  even3prm2  43735  fppr2odd  43747  sbgoldbm  43800  nnsum3primesle9  43810  wtgoldbnnsum4prm  43818  bgoldbnnsum3prm  43820  mgm2mgm  44036  2zrngnmlid  44122  2zrngnmrid  44123  ellcoellss  44392  nneop  44488  fldivexpfllog2  44527  digexp  44569  reorelicc  44599  2itscp  44670  elpglem2  44716
  Copyright terms: Public domain W3C validator