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  2238  cbvalv1  2352  cbval  2407  axc16i  2450  sb3  2495  sb2  2497  axc16gALT  2522  eqrdav  2817  pm13.18OLD  3095  rspcimdv  3610  rspcedv  3613  moi2  3704  moi  3706  sspsstr  4079  2nreu  4389  rabsnifsb  4650  eldifsnneqOLD  4716  ralxfr2d  5301  axprlem4  5317  sbcop1  5370  isso2i  5501  wefrc  5542  elinxp  5883  sotri3  5983  oneqmini  6235  ordsssuc2  6272  ordtri2or  6279  iotan0  6338  2elresin  6461  f1ocnv  6620  tz6.12c  6688  fveqres  6705  fvun1  6747  dffo4  6861  funopsn  6902  fconst5  6960  fnprb  6962  fntpb  6963  isores3  7077  f1owe  7095  weniso  7096  ndmovordi  7328  abnexg  7467  orduniorsuc  7534  ordzsl  7549  tfinds  7563  f1oweALT  7662  opreuopreu  7723  fnse  7816  tposfo2  7904  wfrlem5  7948  wfrlem12  7955  issmo2  7975  iordsmo  7983  smoel2  7989  tz7.48lem  8066  oawordeulem  8169  om00  8190  omlimcl  8193  odi  8194  nnawordi  8236  fiint  8783  fipreima  8818  dffi2  8875  suplub2  8913  wemapsolem  9002  unwdomg  9036  inf3lem3  9081  trcl  9158  fidomtri  9410  prdom2  9420  cardaleph  9503  ackbij1lem16  9645  coflim  9671  coftr  9683  infpssrlem4  9716  isfin7-2  9806  axdc3lem2  9861  axdc3lem4  9863  brdom6disj  9942  entric  9967  fpwwe2lem12  10051  inatsk  10188  grur1a  10229  indpi  10317  reclem3pr  10459  supsrlem  10521  lelttr  10719  dedekindle  10792  negn0  11057  fimaxre  11572  fimaxreOLD  11573  fiminre  11576  nnmulcl  11649  arch  11882  nnnegz  11972  zle0orge1  11986  zeo  12056  uzm1  12264  rpneg  12409  xrlttri  12520  xrlelttr  12537  iccid  12771  icoshft  12847  fzen  12912  elfz1b  12964  elfz2nn0  12986  fleqceilz  13210  zmodidfzoimp  13257  modsumfzodifsn  13300  hasheqf1oi  13700  hashnfinnn0  13710  hashle2prv  13824  swrd0  14008  pfxccatin12lem2  14081  swrdccat  14085  swrdccat3blem  14089  repswswrd  14134  trclublem  14343  max0add  14658  abslt  14662  absle  14663  rexuzre  14700  caurcvg  15021  caucvg  15023  dvdsval2  15598  negdvdsb  15614  muldvds2  15623  dvdsabseq  15651  smuval2  15819  smupvallem  15820  rplpwr  15895  alginv  15907  algfx  15912  coprmgcdb  15981  divgcdcoprm0  15997  oddprmgt2  16031  rpexp1i  16053  qnumdencl  16067  phiprmpw  16101  prmdiveq  16111  prm23lt5  16139  pcmpt  16216  infpnlem1  16234  prmgaplem3  16377  prmgaplem8  16382  imasaddfnlem  16789  plelttr  17570  lubval  17582  lublecllem  17586  glbval  17595  mndind  17980  mndodconglem  18598  sdrgacs  19509  elfrlmbasn0  20835  mavmulsolcl  21088  slesolex  21219  fvmptnn04if  21385  chfacfisf  21390  chfacfisfcpmat  21391  cnpnei  21800  unconn  21965  comppfsc  22068  kqsat  22267  isr0  22273  qtophmeo  22353  trufil  22446  alexsubALT  22587  cnextcn  22603  ucnima  22817  iducn  22819  bl2in  22937  addcnlem  23399  rescncf  23432  ovoliunlem2  24031  voliun  24082  mbflimsup  24194  itgcn  24370  dvdsq1p  24681  aalioulem2  24849  recosf1o  25046  logrec  25268  xrlimcnp  25473  basellem4  25588  bposlem1  25787  bposlem5  25791  lgsqrmod  25855  lgsdchrval  25857  2lgslem1a1  25892  pntlem3  26112  brbtwn2  26618  axbtwnid  26652  elntg2  26698  umgredgprv  26819  umgrpredgv  26852  usgredgprvALT  26904  fusgrfisstep  27038  fusgrfis  27039  nbupgr  27053  nbumgrvtx  27055  finsumvtxdg2size  27259  wlkp1lem8  27389  upgr2pthnlp  27440  wwlksnextinj  27604  usgr2wspthons3  27670  clwwlkccatlem  27694  clwlkclwwlklem2a1  27697  clwwisshclwws  27720  wwlksext2clwwlk  27763  clwwlknonex2lem2  27814  eucrctshift  27949  eucrct2eupth  27951  numclwwlk2lem1  28082  numclwwlk5lem  28093  frgrreggt1  28099  frgrreg  28100  friendship  28105  blocn2  28512  htthlem  28621  axhcompl-zf  28702  spanuni  29248  spansncol  29272  spansneleq  29274  elspansn5  29278  idcnop  29685  pjnormssi  29872  dmdmd  30004  bian1d  30151  ifeqeqx  30224  opabssi  30292  supxrnemnf  30419  rexdiv  30529  xrstos  30593  xrge0omnd  30639  cnre2csqlem  31052  fsumcvg4  31092  lmxrge0  31094  qqhval2lem  31121  esumpr2  31225  esumcvg  31244  issgon  31281  measxun2  31368  measres  31380  measdivcst  31382  measdivcstALTV  31383  elorrvc  31620  signsply0  31720  bnj580  32084  0nn0m1nnn0  32248  umgracycusgr  32298  erdsze2lem2  32348  cvmsval  32410  fmlasuc  32530  fundmpss  32906  dfon2lem3  32927  frmin  32981  poseq  32992  soseq  32993  fprlem1  33034  frrlem15  33039  nosupbnd1  33111  dfrdg4  33309  cgrtriv  33360  btwntriv2  33370  ifscgr  33402  lineext  33434  btwnconn1lem12  33456  colinbtwnle  33476  elicc3  33562  ontgval  33676  onsucconni  33682  bj-bibibi  33817  bj-cbval  33879  bj-cbvex  33880  bj-cbvexw  33906  bj-equsal  34046  bj-restn0  34275  bj-snmoore  34299  bj-elsn0  34339  bj-finsumval0  34455  relowlssretop  34526  sucneqond  34528  finxpsuc  34561  pibt2  34580  wl-nfs1t  34658  finixpnum  34758  ltflcei  34761  matunitlindflem1  34769  poimirlem23  34796  poimirlem24  34797  poimirlem27  34800  poimirlem32  34805  itg2addnclem  34824  areacirclem2  34864  areacirclem5  34867  areacirc  34868  nninfnub  34907  prdstotbnd  34953  heiborlem4  34973  heibor  34980  elghomlem2OLD  35045  grpokerinj  35052  isidlc  35174  prtlem17  35892  dral1-o  35920  axc16g-o  35950  lsator0sp  36017  atlrelat1  36337  cvratlem  36437  diaintclN  38074  dibintclN  38183  cdlemn11pre  38226  dihord2pre  38241  dihintcl  38360  dochkrshp4  38405  lcfrlem9  38566  lcfrlem21  38579  mapdh8e  38800  0prjspnrel  39147  elrfirn2  39171  rencldnfilem  39295  refimssco  39845  rtrclex  39855  intimasn  39880  ss2iundf  39882  ov2ssiunov2  39923  comptiunov2i  39929  iunrelexpuztr  39942  dssmapf1od  40245  mnuprdlem1  40485  mnuprdlem2  40486  snelpwrVD  41042  en3lplem1VD  41054  en3lpVD  41056  orbi1rVD  41059  sbc3orgVD  41062  3impexpVD  41067  equncomVD  41079  trsbcVD  41088  trintALTVD  41091  trintALT  41092  csbingVD  41095  csbsngVD  41104  csbxpgVD  41105  csbrngVD  41107  csbfv12gALTVD  41110  relopabVD  41112  e2ebindVD  41123  xlimpnfxnegmnf  41971  xlimbr  41984  stoweidlem35  42197  stoweidlem48  42210  rexrsb  43175  2reu8i  43189  funbrafv  43234  rlimdmafv  43253  tz6.12c-afv2  43318  rlimdmafv2  43334  fzopredsuc  43400  fzoopth  43404  2ffzoeq  43405  eqfvelsetpreimafv  43430  iccpartlt  43461  proththd  43656  even3prm2  43761  fppr2odd  43773  sbgoldbm  43826  nnsum3primesle9  43836  wtgoldbnnsum4prm  43844  bgoldbnnsum3prm  43846  mgm2mgm  44062  2zrngnmlid  44148  2zrngnmrid  44149  ellcoellss  44418  nneop  44514  fldivexpfllog2  44553  digexp  44595  reorelicc  44625  2itscp  44696  elpglem2  44742
  Copyright terms: Public domain W3C validator