Theorem biimprd 250

Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 222 and biimpri 230. (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 248	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimtrrdi  256  mpbird  259  sylibrd  261  sylbird  262  con4bid  319  mtbid  326  mtbii  328  imbi1d  343  biimpar  481  prlem1  1066  alexbii  1855  speivw  1995  spfw  2055  cbvalw  2057  alcomimw  2065  cbvalv1  2374  cbval  2431  axc16i  2469  sb3  2510  sb2  2512  axc16gALT  2523  ralbida  3275  rspcimdv  3573  rspcedv  3576  moi2  3681  moi  3683  sspsstr  4064  2nreu  4400  rabsnifsb  4683  ralxfr2d  5369  axprlem4OLD  5389  sbcop1  5458  isso2i  5594  wefrc  5643  elinxp  6007  sotri3  6119  oneqmini  6401  ordsssuc2  6441  ordtri2or  6448  iotan0  6513  2elresin  6644  f1ocnv  6821  fveqres  6913  fvun1  6960  dffo4  7086  funopsnOLD  7133  fconst5  7192  fnprb  7194  fntpb  7195  isores3  7321  f1owe  7339  weniso  7340  ndmovordi  7589  abnexg  7741  ordsuc  7796  orduniorsuc  7812  ordzsl  7827  tfinds  7842  dmfexALT  7891  f1oweALT  7955  opreuopreu  8017  fnse  8115  poxp3  8132  poseq  8140  soseq  8141  tposfo2  8231  fprlem1  8283  issmo2  8322  iordsmo  8330  smoel2  8336  tz7.48lem  8414  oawordeulem  8525  om00  8546  omlimcl  8549  odi  8550  nnawordi  8593  unfi  9141  php2  9178  fiint  9273  fipreima  9303  dffi2  9371  suplub2  9409  wemapsolem  9500  unwdomg  9534  inf3lem3  9587  trcl  9685  frrlem15  9717  fidomtri  9953  prdom2  9964  cardaleph  10047  ackbij1lem16  10192  coflim  10220  coftr  10232  infpssrlem4  10265  isfin7-2  10355  axdc3lem2  10410  axdc3lem4  10412  brdom6disj  10491  entric  10516  fpwwe2lem11  10601  inatsk  10738  grur1a  10779  indpi  10867  reclem3pr  11009  supsrlem  11071  lelttr  11275  dedekindle  11349  negn0  11618  fimaxre  12138  fiminre  12141  nnmulcl  12236  arch  12480  nnnegz  12573  zle0orge1  12587  zeo  12661  uzm1  12875  rpneg  13029  xrlttri  13143  xrlelttr  13160  iccid  13396  icoshft  13479  fzen  13548  elfz1b  13600  fzdif1  13612  elfz2nn0  13625  fzoopth  13770  fleqceilz  13866  zmodidfzoimp  13913  modsumfzodifsn  13959  hasheqf1oi  14366  hashnfinnn0  14376  hashle2prv  14493  swrd0  14674  pfxccatin12lem2  14746  swrdccat  14750  swrdccat3blem  14754  repswswrd  14799  trclublem  15010  max0add  15339  abslt  15344  absle  15345  rexuzre  15382  caurcvg  15706  caucvg  15708  dvdsval2  16291  negdvdsb  16308  muldvds2  16317  dvdsabseq  16349  smuval2  16518  smupvallem  16519  rplpwr  16594  alginv  16611  algfx  16616  coprmgcdb  16685  divgcdcoprm0  16701  oddprmgt2  16736  rpexp1i  16760  qnumdencl  16776  phiprmpw  16813  prmdiveq  16823  prm23lt5  16852  pcmpt  16930  infpnlem1  16948  prmgaplem3  17091  prmgaplem8  17096  imasaddfnlem  17560  plelttr  18376  lubval  18388  lublecllem  18392  glbval  18401  mndind  18864  mndodconglem  19583  sdrgacs  20852  xrge0omnd  21499  elfrlmbasn0  21817  mavmulsolcl  22613  slesolex  22744  fvmptnn04if  22911  chfacfisf  22916  chfacfisfcpmat  22917  cnpnei  23326  unconn  23491  comppfsc  23594  kqsat  23793  isr0  23799  qtophmeo  23879  trufil  23972  alexsubALT  24113  cnextcn  24129  ucnima  24342  iducn  24344  bl2in  24462  addcnlem  24927  rescncf  24961  ovoliunlem2  25567  voliun  25618  mbflimsup  25730  itgcn  25909  dvdsq1p  26225  aalioulem2  26399  recosf1o  26602  logrec  26830  xrlimcnp  27035  basellem4  27150  bposlem1  27350  bposlem5  27354  lgsqrmod  27418  lgsdchrval  27420  2lgslem1a1  27455  pntlem3  27675  nosupbnd1  27780  noinfbnd1  27795  oldbday  27996  lrcut  27999  abslts  28344  n0ssoldg  28448  zsoring  28504  bdayfinbndlem1  28562  isplng  28987  brbtwn2  29108  axbtwnid  29142  elntg2  29188  umgredgprv  29310  umgrpredgv  29343  usgredgprvALT  29398  fusgrfisstep  29532  fusgrfis  29533  nbupgr  29547  nbumgrvtx  29549  finsumvtxdg2size  29753  wlkp1lem8  29881  upgr2pthnlp  29934  wwlksnextinj  30101  usgr2wspthons3  30169  clwwlkccatlem  30193  clwlkclwwlklem2a1  30196  clwwisshclwws  30219  wwlksext2clwwlk  30261  clwwlknonex2lem2  30312  eucrctshift  30447  eucrct2eupth  30449  numclwwlk2lem1  30580  numclwwlk5lem  30591  frgrreggt1  30597  frgrreg  30598  friendship  30603  blocn2  31013  htthlem  31122  axhcompl-zf  31203  spanuni  31749  spansncol  31773  spansneleq  31775  elspansn5  31779  idcnop  32186  pjnormssi  32373  dmdmd  32505  bian1dOLD  32660  n0nsnel  32716  ifeqeqx  32743  opabssi  32817  ac6mapd  32827  ressupprn  32894  supxrnemnf  32972  rexdiv  33105  xrstos  33190  cnre2csqlem  34209  fsumcvg4  34249  lmxrge0  34251  qqhval2lem  34280  esumpr2  34366  esumcvg  34385  issgon  34422  measxun2  34509  measres  34521  measdivcst  34523  measdivcstALTV  34524  elorrvc  34763  signsply0  34847  bnj580  35210  nummin  35391  axprALT2  35409  0nn0m1nnn0  35467  umgracycusgr  35509  erdsze2lem2  35559  cvmsval  35621  fmlasuc  35741  fundmpss  36122  dfon2lem3  36138  dfrdg4  36306  cgrtriv  36357  btwntriv2  36367  ifscgr  36399  lineext  36431  btwnconn1lem12  36453  colinbtwnle  36473  elicc3  36682  ontgval  36796  onsucconni  36802  axtco1from2  36840  axtcond  36843  axnulregtco  36845  dfttc4lem2  36894  bj-bibibi  37034  bj-cbvalvv  37116  bj-cbval  37123  bj-cbvex  37124  bj-cbvexw  37154  bj-nnf-cbval  37260  bj-equsal  37316  bj-gabeqd  37427  bj-restn0  37585  bj-snmoore  37608  cgsex2gd  37634  bj-elsn0  37652  bj-finsumval0  37782  relowlssretop  37862  sucneqond  37864  finxpsuc  37897  pibt2  37916  wl-nfs1t  38045  finixpnum  38109  ltflcei  38112  matunitlindflem1  38120  poimirlem23  38147  poimirlem24  38148  poimirlem27  38151  poimirlem32  38156  itg2addnclem  38175  areacirclem2  38213  areacirclem5  38216  areacirc  38217  nninfnub  38255  prdstotbnd  38298  heiborlem4  38318  heibor  38325  elghomlem2OLD  38390  grpokerinj  38397  isidlc  38519  disjlem17  39406  prtlem17  39505  dral1-o  39533  axc16g-o  39563  lsator0sp  39630  atlrelat1  39950  cvratlem  40050  diaintclN  41687  dibintclN  41796  cdlemn11pre  41839  dihord2pre  41854  dihintcl  41973  dochkrshp4  42018  lcfrlem9  42179  lcfrlem21  42192  mapdh8e  42413  aks4d1p5  42702  aks6d1c1p1  42729  sticksstones4  42771  0prjspnrel  43214  elrfirn2  43282  rencldnfilem  43402  onsupnmax  43810  onov0suclim  43856  oege1  43888  cantnfresb  43906  dflim5  43911  omabs2  43914  refimssco  44188  rtrclex  44198  intimasn  44238  ss2iundf  44240  ov2ssiunov2  44281  comptiunov2i  44287  iunrelexpuztr  44300  dssmapf1od  44602  mnringmulrcld  44809  mnuprdlem1  44853  mnuprdlem2  44854  snelpwrVD  45411  en3lplem1VD  45423  en3lpVD  45425  orbi1rVD  45428  sbc3orgVD  45431  3impexpVD  45436  equncomVD  45448  trsbcVD  45457  trintALTVD  45460  trintALT  45461  csbingVD  45464  csbsngVD  45473  csbxpgVD  45474  csbrngVD  45476  csbfv12gALTVD  45479  relopabVD  45481  e2ebindVD  45492  xlimpnfxnegmnf  46393  xlimbr  46406  stoweidlem35  46614  stoweidlem48  46627  ormkglobd  47456  cjnpoly  47488  tannpoly  47489  n0nsn2el  47624  rexrsb  47699  2reu8i  47712  funbrafv  47757  rlimdmafv  47776  tz6.12c-afv2  47841  rlimdmafv2  47857  fzopredsuc  47923  2ffzoeq  47927  m1modnep2mod  47957  2timesltsq  47977  eqfvelsetpreimafv  48004  iccpartlt  48035  proththd  48228  even3prm2  48346  fppr2odd  48358  sbgoldbm  48411  nnsum3primesle9  48421  wtgoldbnnsum4prm  48429  bgoldbnnsum3prm  48431  grtrif1o  48569  mgm2mgm  48854  2zrngnmlid  48882  2zrngnmrid  48883  ellcoellss  49062  nneop  49153  fldivexpfllog2  49192  digexp  49234  reorelicc  49337  2itscp  49408  oppc1stflem  49913  prsthinc  50090  elpglem2  50338