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  1046  alexbii  1824  speivw  1968  spfw  2031  cbvalw  2033  alcomiw  2041  alcomiwOLD  2042  sbbidvOLD  2076  sbbidOLD  2239  cbvalv1  2353  cbval  2410  axc16i  2453  sb3  2498  sb2  2500  axc16gALT  2525  eqrdav  2820  pm13.18OLD  3098  rspcimdv  3612  rspcedv  3615  moi2  3706  moi  3708  sspsstr  4081  2nreu  4391  rabsnifsb  4652  eldifsnneqOLD  4718  ralxfr2d  5302  axprlem4  5318  sbcop1  5371  isso2i  5502  wefrc  5543  elinxp  5884  sotri3  5984  oneqmini  6236  ordsssuc2  6273  ordtri2or  6280  iotan0  6339  2elresin  6462  f1ocnv  6621  tz6.12c  6689  fveqres  6706  fvun1  6748  dffo4  6862  funopsn  6903  fconst5  6961  fnprb  6963  fntpb  6964  isores3  7077  f1owe  7095  weniso  7096  ndmovordi  7328  abnexg  7466  orduniorsuc  7533  ordzsl  7548  tfinds  7562  f1oweALT  7664  opreuopreu  7725  fnse  7818  tposfo2  7906  wfrlem5  7950  wfrlem12  7957  issmo2  7977  iordsmo  7985  smoel2  7991  tz7.48lem  8068  oawordeulem  8170  om00  8191  omlimcl  8194  odi  8195  nnawordi  8237  fiint  8784  fipreima  8819  dffi2  8876  suplub2  8914  wemapsolem  9003  unwdomg  9037  inf3lem3  9082  trcl  9159  fidomtri  9411  prdom2  9421  cardaleph  9504  ackbij1lem16  9646  coflim  9672  coftr  9684  infpssrlem4  9717  isfin7-2  9807  axdc3lem2  9862  axdc3lem4  9864  brdom6disj  9943  entric  9968  fpwwe2lem12  10052  inatsk  10189  grur1a  10230  indpi  10318  reclem3pr  10460  supsrlem  10522  lelttr  10720  dedekindle  10793  negn0  11058  fimaxre  11573  fimaxreOLD  11574  fiminre  11577  nnmulcl  11650  arch  11883  nnnegz  11973  zle0orge1  11987  zeo  12057  uzm1  12265  rpneg  12411  xrlttri  12522  xrlelttr  12539  iccid  12773  icoshft  12849  fzen  12914  elfz1b  12966  elfz2nn0  12988  fleqceilz  13212  zmodidfzoimp  13259  modsumfzodifsn  13302  hasheqf1oi  13702  hashnfinnn0  13712  hashle2prv  13826  swrd0  14010  pfxccatin12lem2  14083  swrdccat  14087  swrdccat3blem  14091  repswswrd  14136  trclublem  14345  max0add  14660  abslt  14664  absle  14665  rexuzre  14702  caurcvg  15023  caucvg  15025  dvdsval2  15600  negdvdsb  15616  muldvds2  15625  dvdsabseq  15653  smuval2  15821  smupvallem  15822  rplpwr  15897  alginv  15909  algfx  15914  coprmgcdb  15983  divgcdcoprm0  15999  oddprmgt2  16033  rpexp1i  16055  qnumdencl  16069  phiprmpw  16103  prmdiveq  16113  prm23lt5  16141  pcmpt  16218  infpnlem1  16236  prmgaplem3  16379  prmgaplem8  16384  imasaddfnlem  16791  plelttr  17572  lubval  17584  lublecllem  17588  glbval  17597  mndind  17982  mndodconglem  18600  sdrgacs  19511  elfrlmbasn0  20837  mavmulsolcl  21090  slesolex  21221  fvmptnn04if  21387  chfacfisf  21392  chfacfisfcpmat  21393  cnpnei  21802  unconn  21967  comppfsc  22070  kqsat  22269  isr0  22275  qtophmeo  22355  trufil  22448  alexsubALT  22589  cnextcn  22605  ucnima  22819  iducn  22821  bl2in  22939  addcnlem  23401  rescncf  23434  ovoliunlem2  24033  voliun  24084  mbflimsup  24196  itgcn  24372  dvdsq1p  24683  aalioulem2  24851  recosf1o  25046  logrec  25268  xrlimcnp  25474  basellem4  25589  bposlem1  25788  bposlem5  25792  lgsqrmod  25856  lgsdchrval  25858  2lgslem1a1  25893  pntlem3  26113  brbtwn2  26619  axbtwnid  26653  elntg2  26699  umgredgprv  26820  umgrpredgv  26853  usgredgprvALT  26905  fusgrfisstep  27039  fusgrfis  27040  nbupgr  27054  nbumgrvtx  27056  finsumvtxdg2size  27260  wlkp1lem8  27390  upgr2pthnlp  27441  wwlksnextinj  27605  usgr2wspthons3  27671  clwwlkccatlem  27695  clwlkclwwlklem2a1  27698  clwwisshclwws  27721  wwlksext2clwwlk  27764  clwwlknonex2lem2  27815  eucrctshift  27950  eucrct2eupth  27952  numclwwlk2lem1  28083  numclwwlk5lem  28094  frgrreggt1  28100  frgrreg  28101  friendship  28106  blocn2  28513  htthlem  28622  axhcompl-zf  28703  spanuni  29249  spansncol  29273  spansneleq  29275  elspansn5  29279  idcnop  29686  pjnormssi  29873  dmdmd  30005  bian1d  30152  ifeqeqx  30225  opabssi  30293  supxrnemnf  30420  rexdiv  30530  xrstos  30594  xrge0omnd  30640  cnre2csqlem  31053  fsumcvg4  31093  lmxrge0  31095  qqhval2lem  31122  esumpr2  31226  esumcvg  31245  issgon  31282  measxun2  31369  measres  31381  measdivcst  31383  measdivcstALTV  31384  elorrvc  31621  signsply0  31721  bnj580  32085  0nn0m1nnn0  32249  umgracycusgr  32299  erdsze2lem2  32349  cvmsval  32411  fmlasuc  32531  fundmpss  32907  dfon2lem3  32928  frmin  32982  poseq  32993  soseq  32994  fprlem1  33035  frrlem15  33040  nosupbnd1  33112  dfrdg4  33310  cgrtriv  33361  btwntriv2  33371  ifscgr  33403  lineext  33435  btwnconn1lem12  33457  colinbtwnle  33477  elicc3  33563  ontgval  33677  onsucconni  33683  bj-bibibi  33818  bj-cbval  33880  bj-cbvex  33881  bj-cbvexw  33907  bj-equsal  34047  bj-restn0  34276  bj-snmoore  34300  bj-elsn0  34340  bj-finsumval0  34456  relowlssretop  34527  sucneqond  34529  finxpsuc  34562  pibt2  34581  wl-nfs1t  34659  finixpnum  34759  ltflcei  34762  matunitlindflem1  34770  poimirlem23  34797  poimirlem24  34798  poimirlem27  34801  poimirlem32  34806  itg2addnclem  34825  areacirclem2  34865  areacirclem5  34868  areacirc  34869  nninfnub  34909  prdstotbnd  34955  heiborlem4  34975  heibor  34982  elghomlem2OLD  35047  grpokerinj  35054  isidlc  35176  prtlem17  35894  dral1-o  35922  axc16g-o  35952  lsator0sp  36019  atlrelat1  36339  cvratlem  36439  diaintclN  38076  dibintclN  38185  cdlemn11pre  38228  dihord2pre  38243  dihintcl  38362  dochkrshp4  38407  lcfrlem9  38568  lcfrlem21  38581  mapdh8e  38802  0prjspnrel  39149  elrfirn2  39173  rencldnfilem  39297  refimssco  39847  rtrclex  39857  intimasn  39882  ss2iundf  39884  ov2ssiunov2  39925  comptiunov2i  39931  iunrelexpuztr  39944  dssmapf1od  40247  mnuprdlem1  40488  mnuprdlem2  40489  snelpwrVD  41045  en3lplem1VD  41057  en3lpVD  41059  orbi1rVD  41062  sbc3orgVD  41065  3impexpVD  41070  equncomVD  41082  trsbcVD  41091  trintALTVD  41094  trintALT  41095  csbingVD  41098  csbsngVD  41107  csbxpgVD  41108  csbrngVD  41110  csbfv12gALTVD  41113  relopabVD  41115  e2ebindVD  41126  xlimpnfxnegmnf  41975  xlimbr  41988  stoweidlem35  42201  stoweidlem48  42214  rexrsb  43179  2reu8i  43193  funbrafv  43238  rlimdmafv  43257  tz6.12c-afv2  43322  rlimdmafv2  43338  fzopredsuc  43404  fzoopth  43408  2ffzoeq  43409  iccpartlt  43431  proththd  43626  even3prm2  43731  fppr2odd  43743  sbgoldbm  43796  nnsum3primesle9  43806  wtgoldbnnsum4prm  43814  bgoldbnnsum3prm  43816  mgm2mgm  44032  2zrngnmlid  44118  2zrngnmrid  44119  ellcoellss  44388  nneop  44484  fldivexpfllog2  44523  digexp  44565  reorelicc  44595  2itscp  44666  elpglem2  44712
  Copyright terms: Public domain W3C validator