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  1835  speivw  1975  spfw  2035  cbvalw  2037  alcomimw  2045  cbvalv1  2344  cbval  2401  axc16i  2439  sb3  2480  sb2  2482  axc16gALT  2493  eqrdav  2734  ralbida  3246  rspcimdv  3565  rspcedv  3568  moi2  3673  moi  3675  sspsstr  4059  2nreu  4395  rabsnifsb  4678  ralxfr2d  5354  axprlem4OLD  5373  sbcop1  5435  isso2i  5568  wefrc  5617  elinxp  5977  sotri3  6086  oneqmini  6369  ordsssuc2  6409  ordtri2or  6416  iotan0  6481  2elresin  6612  f1ocnv  6785  fveqres  6877  fvun1  6924  dffo4  7048  funopsn  7093  fconst5  7152  fnprb  7154  fntpb  7155  isores3  7281  f1owe  7299  weniso  7300  ndmovordi  7549  abnexg  7701  ordsuc  7756  orduniorsuc  7772  ordzsl  7787  tfinds  7802  dmfexALT  7850  f1oweALT  7916  opreuopreu  7978  fnse  8075  poxp3  8092  poseq  8100  soseq  8101  tposfo2  8191  fprlem1  8242  issmo2  8281  iordsmo  8289  smoel2  8295  tz7.48lem  8372  oawordeulem  8481  om00  8502  omlimcl  8505  odi  8506  nnawordi  8549  unfi  9097  php2  9134  fiint  9229  fipreima  9260  dffi2  9328  suplub2  9366  wemapsolem  9457  unwdomg  9491  inf3lem3  9541  trcl  9639  frrlem15  9671  fidomtri  9907  prdom2  9918  cardaleph  10001  ackbij1lem16  10146  coflim  10173  coftr  10185  infpssrlem4  10218  isfin7-2  10308  axdc3lem2  10363  axdc3lem4  10365  brdom6disj  10444  entric  10469  fpwwe2lem11  10554  inatsk  10691  grur1a  10732  indpi  10820  reclem3pr  10962  supsrlem  11024  lelttr  11225  dedekindle  11299  negn0  11568  fimaxre  12088  fiminre  12091  nnmulcl  12171  arch  12400  nnnegz  12493  zle0orge1  12507  zeo  12580  uzm1  12787  rpneg  12941  xrlttri  13055  xrlelttr  13072  iccid  13308  icoshft  13391  fzen  13459  elfz1b  13511  fzdif1  13523  elfz2nn0  13536  fzoopth  13680  fleqceilz  13776  zmodidfzoimp  13823  modsumfzodifsn  13869  hasheqf1oi  14276  hashnfinnn0  14286  hashle2prv  14403  swrd0  14584  pfxccatin12lem2  14656  swrdccat  14660  swrdccat3blem  14664  repswswrd  14709  trclublem  14920  max0add  15235  abslt  15240  absle  15241  rexuzre  15278  caurcvg  15602  caucvg  15604  dvdsval2  16184  negdvdsb  16201  muldvds2  16210  dvdsabseq  16242  smuval2  16411  smupvallem  16412  rplpwr  16487  alginv  16504  algfx  16509  coprmgcdb  16578  divgcdcoprm0  16594  oddprmgt2  16628  rpexp1i  16652  qnumdencl  16668  phiprmpw  16705  prmdiveq  16715  prm23lt5  16744  pcmpt  16822  infpnlem1  16840  prmgaplem3  16983  prmgaplem8  16988  imasaddfnlem  17451  plelttr  18267  lubval  18279  lublecllem  18283  glbval  18292  mndind  18755  mndodconglem  19472  sdrgacs  20736  xrge0omnd  21402  elfrlmbasn0  21720  mavmulsolcl  22497  slesolex  22628  fvmptnn04if  22795  chfacfisf  22800  chfacfisfcpmat  22801  cnpnei  23210  unconn  23375  comppfsc  23478  kqsat  23677  isr0  23683  qtophmeo  23763  trufil  23856  alexsubALT  23997  cnextcn  24013  ucnima  24226  iducn  24228  bl2in  24346  addcnlem  24811  rescncf  24848  ovoliunlem2  25462  voliun  25513  mbflimsup  25625  itgcn  25804  dvdsq1p  26126  aalioulem2  26299  recosf1o  26502  logrec  26731  xrlimcnp  26936  basellem4  27052  bposlem1  27253  bposlem5  27257  lgsqrmod  27321  lgsdchrval  27323  2lgslem1a1  27358  pntlem3  27578  nosupbnd1  27684  noinfbnd1  27699  oldbday  27881  lrcut  27884  absslt  28228  n0ssoldg  28331  zsoring  28386  bdayfinbndlem1  28444  brbtwn2  28959  axbtwnid  28993  elntg2  29039  umgredgprv  29161  umgrpredgv  29194  usgredgprvALT  29249  fusgrfisstep  29383  fusgrfis  29384  nbupgr  29398  nbumgrvtx  29400  finsumvtxdg2size  29605  wlkp1lem8  29733  upgr2pthnlp  29786  wwlksnextinj  29953  usgr2wspthons3  30021  clwwlkccatlem  30045  clwlkclwwlklem2a1  30048  clwwisshclwws  30071  wwlksext2clwwlk  30113  clwwlknonex2lem2  30164  eucrctshift  30299  eucrct2eupth  30301  numclwwlk2lem1  30432  numclwwlk5lem  30443  frgrreggt1  30449  frgrreg  30450  friendship  30455  blocn2  30864  htthlem  30973  axhcompl-zf  31054  spanuni  31600  spansncol  31624  spansneleq  31626  elspansn5  31630  idcnop  32037  pjnormssi  32224  dmdmd  32356  bian1dOLD  32511  n0nsnel  32570  ifeqeqx  32597  opabssi  32671  ac6mapd  32681  ressupprn  32748  supxrnemnf  32827  rexdiv  32986  xrstos  33071  cnre2csqlem  34046  fsumcvg4  34086  lmxrge0  34088  qqhval2lem  34117  esumpr2  34203  esumcvg  34222  issgon  34259  measxun2  34346  measres  34358  measdivcst  34360  measdivcstALTV  34361  elorrvc  34600  signsply0  34687  bnj580  35048  nummin  35228  0nn0m1nnn0  35286  umgracycusgr  35327  erdsze2lem2  35377  cvmsval  35439  fmlasuc  35559  fundmpss  35940  dfon2lem3  35956  dfrdg4  36124  cgrtriv  36175  btwntriv2  36185  ifscgr  36217  lineext  36249  btwnconn1lem12  36271  colinbtwnle  36291  elicc3  36490  ontgval  36604  onsucconni  36610  bj-bibibi  36759  bj-cbval  36822  bj-cbvex  36823  bj-cbvexw  36850  bj-equsal  37000  bj-gabeqd  37111  bj-restn0  37264  bj-snmoore  37287  bj-elsn0  37329  bj-finsumval0  37459  relowlssretop  37537  sucneqond  37539  finxpsuc  37572  pibt2  37591  wl-nfs1t  37711  finixpnum  37775  ltflcei  37778  matunitlindflem1  37786  poimirlem23  37813  poimirlem24  37814  poimirlem27  37817  poimirlem32  37822  itg2addnclem  37841  areacirclem2  37879  areacirclem5  37882  areacirc  37883  nninfnub  37921  prdstotbnd  37964  heiborlem4  37984  heibor  37991  elghomlem2OLD  38056  grpokerinj  38063  isidlc  38185  disjlem17  39072  prtlem17  39171  dral1-o  39199  axc16g-o  39229  lsator0sp  39296  atlrelat1  39616  cvratlem  39716  diaintclN  41353  dibintclN  41462  cdlemn11pre  41505  dihord2pre  41520  dihintcl  41639  dochkrshp4  41684  lcfrlem9  41845  lcfrlem21  41858  mapdh8e  42079  aks4d1p5  42369  aks6d1c1p1  42396  sticksstones4  42438  0prjspnrel  42907  elrfirn2  42975  rencldnfilem  43099  onsupnmax  43507  onov0suclim  43553  oege1  43585  cantnfresb  43603  dflim5  43608  omabs2  43611  refimssco  43885  rtrclex  43895  intimasn  43935  ss2iundf  43937  ov2ssiunov2  43978  comptiunov2i  43984  iunrelexpuztr  43997  dssmapf1od  44299  mnringmulrcld  44506  mnuprdlem1  44550  mnuprdlem2  44551  snelpwrVD  45108  en3lplem1VD  45120  en3lpVD  45122  orbi1rVD  45125  sbc3orgVD  45128  3impexpVD  45133  equncomVD  45145  trsbcVD  45154  trintALTVD  45157  trintALT  45158  csbingVD  45161  csbsngVD  45170  csbxpgVD  45171  csbrngVD  45173  csbfv12gALTVD  45176  relopabVD  45178  e2ebindVD  45189  xlimpnfxnegmnf  46095  xlimbr  46108  stoweidlem35  46316  stoweidlem48  46329  ormkglobd  47156  cjnpoly  47172  tannpoly  47173  n0nsn2el  47308  rexrsb  47383  2reu8i  47396  funbrafv  47441  rlimdmafv  47460  tz6.12c-afv2  47525  rlimdmafv2  47541  fzopredsuc  47606  2ffzoeq  47610  m1modnep2mod  47635  eqfvelsetpreimafv  47676  iccpartlt  47707  proththd  47897  even3prm2  48002  fppr2odd  48014  sbgoldbm  48067  nnsum3primesle9  48077  wtgoldbnnsum4prm  48085  bgoldbnnsum3prm  48087  grtrif1o  48225  mgm2mgm  48510  2zrngnmlid  48538  2zrngnmrid  48539  ellcoellss  48718  nneop  48809  fldivexpfllog2  48848  digexp  48890  reorelicc  48993  2itscp  49064  oppc1stflem  49569  prsthinc  49746  elpglem2  49994