Theorem biimprd 248

Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 220 and biimpri 228. (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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜒 → 𝜒)
2		biimprd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	imbitrrid 246	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimtrrdi  254  mpbird  257  sylibrd  259  sylbird  260  con4bid  317  mtbid  324  mtbii  326  imbi1d  341  biimpar  477  prlem1  1055  alexbii  1833  speivw  1973  spfw  2032  cbvalw  2034  alcomimw  2042  cbvalv1  2343  cbval  2403  axc16i  2441  sb3  2482  sb2  2484  axc16gALT  2495  eqrdav  2736  ralbida  3270  rspcimdv  3612  rspcedv  3615  moi2  3722  moi  3724  sspsstr  4108  2nreu  4444  rabsnifsb  4722  ralxfr2d  5410  axprlem4OLD  5429  sbcop1  5493  isso2i  5629  wefrc  5679  elinxp  6037  sotri3  6150  oneqmini  6436  ordsssuc2  6475  ordtri2or  6482  iotan0  6551  2elresin  6689  f1ocnv  6860  tz6.12cOLD  6933  fveqres  6953  fvun1  7000  dffo4  7123  funopsn  7168  fconst5  7226  fnprb  7228  fntpb  7229  isores3  7355  f1owe  7373  weniso  7374  ndmovordi  7624  abnexg  7776  ordsuc  7833  orduniorsuc  7850  ordzsl  7866  tfinds  7881  dmfexALT  7930  f1oweALT  7997  opreuopreu  8059  fnse  8158  poxp3  8175  poseq  8183  soseq  8184  tposfo2  8274  fprlem1  8325  wfrlem5OLD  8353  wfrlem12OLD  8360  issmo2  8389  iordsmo  8397  smoel2  8403  tz7.48lem  8481  oawordeulem  8592  om00  8613  omlimcl  8616  odi  8617  nnawordi  8659  unfi  9211  php2  9248  fiint  9366  fiintOLD  9367  fipreima  9398  dffi2  9463  suplub2  9501  wemapsolem  9590  unwdomg  9624  inf3lem3  9670  trcl  9768  frrlem15  9797  fidomtri  10033  prdom2  10046  cardaleph  10129  ackbij1lem16  10274  coflim  10301  coftr  10313  infpssrlem4  10346  isfin7-2  10436  axdc3lem2  10491  axdc3lem4  10493  brdom6disj  10572  entric  10597  fpwwe2lem11  10681  inatsk  10818  grur1a  10859  indpi  10947  reclem3pr  11089  supsrlem  11151  lelttr  11351  dedekindle  11425  negn0  11692  fimaxre  12212  fiminre  12215  nnmulcl  12290  arch  12523  nnnegz  12616  zle0orge1  12630  zeo  12704  uzm1  12916  rpneg  13067  xrlttri  13181  xrlelttr  13198  iccid  13432  icoshft  13513  fzen  13581  elfz1b  13633  fzdif1  13645  elfz2nn0  13658  fzoopth  13801  fleqceilz  13894  zmodidfzoimp  13941  modsumfzodifsn  13985  hasheqf1oi  14390  hashnfinnn0  14400  hashle2prv  14517  swrd0  14696  pfxccatin12lem2  14769  swrdccat  14773  swrdccat3blem  14777  repswswrd  14822  trclublem  15034  max0add  15349  abslt  15353  absle  15354  rexuzre  15391  caurcvg  15713  caucvg  15715  dvdsval2  16293  negdvdsb  16310  muldvds2  16319  dvdsabseq  16350  smuval2  16519  smupvallem  16520  rplpwr  16595  alginv  16612  algfx  16617  coprmgcdb  16686  divgcdcoprm0  16702  oddprmgt2  16736  rpexp1i  16760  qnumdencl  16776  phiprmpw  16813  prmdiveq  16823  prm23lt5  16852  pcmpt  16930  infpnlem1  16948  prmgaplem3  17091  prmgaplem8  17096  imasaddfnlem  17573  plelttr  18389  lubval  18401  lublecllem  18405  glbval  18414  mndind  18841  mndodconglem  19559  sdrgacs  20802  elfrlmbasn0  21783  mavmulsolcl  22557  slesolex  22688  fvmptnn04if  22855  chfacfisf  22860  chfacfisfcpmat  22861  cnpnei  23272  unconn  23437  comppfsc  23540  kqsat  23739  isr0  23745  qtophmeo  23825  trufil  23918  alexsubALT  24059  cnextcn  24075  ucnima  24290  iducn  24292  bl2in  24410  addcnlem  24886  rescncf  24923  ovoliunlem2  25538  voliun  25589  mbflimsup  25701  itgcn  25880  dvdsq1p  26202  aalioulem2  26375  recosf1o  26577  logrec  26806  xrlimcnp  27011  basellem4  27127  bposlem1  27328  bposlem5  27332  lgsqrmod  27396  lgsdchrval  27398  2lgslem1a1  27433  pntlem3  27653  nosupbnd1  27759  noinfbnd1  27774  oldbday  27939  lrcut  27941  absslt  28273  brbtwn2  28920  axbtwnid  28954  elntg2  29000  umgredgprv  29124  umgrpredgv  29157  usgredgprvALT  29212  fusgrfisstep  29346  fusgrfis  29347  nbupgr  29361  nbumgrvtx  29363  finsumvtxdg2size  29568  wlkp1lem8  29698  upgr2pthnlp  29752  wwlksnextinj  29919  usgr2wspthons3  29984  clwwlkccatlem  30008  clwlkclwwlklem2a1  30011  clwwisshclwws  30034  wwlksext2clwwlk  30076  clwwlknonex2lem2  30127  eucrctshift  30262  eucrct2eupth  30264  numclwwlk2lem1  30395  numclwwlk5lem  30406  frgrreggt1  30412  frgrreg  30413  friendship  30418  blocn2  30827  htthlem  30936  axhcompl-zf  31017  spanuni  31563  spansncol  31587  spansneleq  31589  elspansn5  31593  idcnop  32000  pjnormssi  32187  dmdmd  32319  bian1dOLD  32476  n0nsnel  32534  ifeqeqx  32555  opabssi  32625  ac6mapd  32635  ressupprn  32699  supxrnemnf  32772  rexdiv  32908  xrstos  33012  xrge0omnd  33088  cnre2csqlem  33909  fsumcvg4  33949  lmxrge0  33951  qqhval2lem  33982  esumpr2  34068  esumcvg  34087  issgon  34124  measxun2  34211  measres  34223  measdivcst  34225  measdivcstALTV  34226  elorrvc  34466  signsply0  34566  bnj580  34927  nummin  35105  0nn0m1nnn0  35118  umgracycusgr  35159  erdsze2lem2  35209  cvmsval  35271  fmlasuc  35391  fundmpss  35767  dfon2lem3  35786  dfrdg4  35952  cgrtriv  36003  btwntriv2  36013  ifscgr  36045  lineext  36077  btwnconn1lem12  36099  colinbtwnle  36119  elicc3  36318  ontgval  36432  onsucconni  36438  bj-bibibi  36587  bj-cbval  36650  bj-cbvex  36651  bj-cbvexw  36677  bj-equsal  36827  bj-gabeqd  36938  bj-restn0  37091  bj-snmoore  37114  bj-elsn0  37156  bj-finsumval0  37286  relowlssretop  37364  sucneqond  37366  finxpsuc  37399  pibt2  37418  wl-nfs1t  37538  finixpnum  37612  ltflcei  37615  matunitlindflem1  37623  poimirlem23  37650  poimirlem24  37651  poimirlem27  37654  poimirlem32  37659  itg2addnclem  37678  areacirclem2  37716  areacirclem5  37719  areacirc  37720  nninfnub  37758  prdstotbnd  37801  heiborlem4  37821  heibor  37828  elghomlem2OLD  37893  grpokerinj  37900  isidlc  38022  disjlem17  38800  prtlem17  38877  dral1-o  38905  axc16g-o  38935  lsator0sp  39002  atlrelat1  39322  cvratlem  39423  diaintclN  41060  dibintclN  41169  cdlemn11pre  41212  dihord2pre  41227  dihintcl  41346  dochkrshp4  41391  lcfrlem9  41552  lcfrlem21  41565  mapdh8e  41786  aks4d1p5  42081  aks6d1c1p1  42108  sticksstones4  42150  metakunt29  42234  0prjspnrel  42637  elrfirn2  42707  rencldnfilem  42831  onsupnmax  43240  onov0suclim  43287  oege1  43319  cantnfresb  43337  dflim5  43342  omabs2  43345  refimssco  43620  rtrclex  43630  intimasn  43670  ss2iundf  43672  ov2ssiunov2  43713  comptiunov2i  43719  iunrelexpuztr  43732  dssmapf1od  44034  mnringmulrcld  44247  mnuprdlem1  44291  mnuprdlem2  44292  snelpwrVD  44851  en3lplem1VD  44863  en3lpVD  44865  orbi1rVD  44868  sbc3orgVD  44871  3impexpVD  44876  equncomVD  44888  trsbcVD  44897  trintALTVD  44900  trintALT  44901  csbingVD  44904  csbsngVD  44913  csbxpgVD  44914  csbrngVD  44916  csbfv12gALTVD  44919  relopabVD  44921  e2ebindVD  44932  xlimpnfxnegmnf  45829  xlimbr  45842  stoweidlem35  46050  stoweidlem48  46063  ormkglobd  46890  n0nsn2el  47037  rexrsb  47112  2reu8i  47125  funbrafv  47170  rlimdmafv  47189  tz6.12c-afv2  47254  rlimdmafv2  47270  fzopredsuc  47335  2ffzoeq  47339  m1modnep2mod  47354  eqfvelsetpreimafv  47380  iccpartlt  47411  proththd  47601  even3prm2  47706  fppr2odd  47718  sbgoldbm  47771  nnsum3primesle9  47781  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  grtrif1o  47909  mgm2mgm  48143  2zrngnmlid  48171  2zrngnmrid  48172  ellcoellss  48352  nneop  48447  fldivexpfllog2  48486  digexp  48528  reorelicc  48631  2itscp  48702  prsthinc  49111  elpglem2  49231