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  479  prlem1  1061  alexbii  1841  speivw  1981  spfw  2041  cbvalw  2043  alcomimw  2051  cbvalv1  2351  cbval  2408  axc16i  2446  sb3  2487  sb2  2489  axc16gALT  2500  ralbida  3252  rspcimdv  3552  rspcedv  3555  moi2  3659  moi  3661  sspsstr  4042  2nreu  4375  rabsnifsb  4657  ralxfr2d  5342  axprlem4OLD  5362  sbcop1  5431  isso2i  5566  wefrc  5615  elinxp  5978  sotri3  6087  oneqmini  6367  ordsssuc2  6407  ordtri2or  6414  iotan0  6479  2elresin  6610  f1ocnv  6783  fveqres  6875  fvun1  6922  dffo4  7048  funopsnOLD  7095  fconst5  7154  fnprb  7156  fntpb  7157  isores3  7283  f1owe  7301  weniso  7302  ndmovordi  7551  abnexg  7703  ordsuc  7758  orduniorsuc  7774  ordzsl  7789  tfinds  7804  dmfexALT  7852  f1oweALT  7918  opreuopreu  7980  fnse  8077  poxp3  8094  poseq  8102  soseq  8103  tposfo2  8193  fprlem1  8244  issmo2  8283  iordsmo  8291  smoel2  8297  tz7.48lem  8374  oawordeulem  8483  om00  8504  omlimcl  8507  odi  8508  nnawordi  8551  unfi  9099  php2  9136  fiint  9231  fipreima  9262  dffi2  9330  suplub2  9368  wemapsolem  9459  unwdomg  9493  inf3lem3  9546  trcl  9644  frrlem15  9676  fidomtri  9912  prdom2  9923  cardaleph  10006  ackbij1lem16  10151  coflim  10178  coftr  10190  infpssrlem4  10223  isfin7-2  10313  axdc3lem2  10368  axdc3lem4  10370  brdom6disj  10449  entric  10474  fpwwe2lem11  10559  inatsk  10696  grur1a  10737  indpi  10825  reclem3pr  10967  supsrlem  11029  lelttr  11231  dedekindle  11305  negn0  11574  fimaxre  12095  fiminre  12098  nnmulcl  12193  arch  12429  nnnegz  12522  zle0orge1  12536  zeo  12610  uzm1  12817  rpneg  12971  xrlttri  13085  xrlelttr  13102  iccid  13338  icoshft  13421  fzen  13490  elfz1b  13542  fzdif1  13554  elfz2nn0  13567  fzoopth  13712  fleqceilz  13808  zmodidfzoimp  13855  modsumfzodifsn  13901  hasheqf1oi  14308  hashnfinnn0  14318  hashle2prv  14435  swrd0  14616  pfxccatin12lem2  14688  swrdccat  14692  swrdccat3blem  14696  repswswrd  14741  trclublem  14952  max0add  15267  abslt  15272  absle  15273  rexuzre  15310  caurcvg  15634  caucvg  15636  dvdsval2  16219  negdvdsb  16236  muldvds2  16245  dvdsabseq  16277  smuval2  16446  smupvallem  16447  rplpwr  16522  alginv  16539  algfx  16544  coprmgcdb  16613  divgcdcoprm0  16629  oddprmgt2  16664  rpexp1i  16688  qnumdencl  16704  phiprmpw  16741  prmdiveq  16751  prm23lt5  16780  pcmpt  16858  infpnlem1  16876  prmgaplem3  17019  prmgaplem8  17024  imasaddfnlem  17487  plelttr  18303  lubval  18315  lublecllem  18319  glbval  18328  mndind  18791  mndodconglem  19511  sdrgacs  20777  xrge0omnd  21424  elfrlmbasn0  21742  mavmulsolcl  22538  slesolex  22669  fvmptnn04if  22836  chfacfisf  22841  chfacfisfcpmat  22842  cnpnei  23251  unconn  23416  comppfsc  23519  kqsat  23718  isr0  23724  qtophmeo  23804  trufil  23897  alexsubALT  24038  cnextcn  24054  ucnima  24267  iducn  24269  bl2in  24387  addcnlem  24852  rescncf  24886  ovoliunlem2  25492  voliun  25543  mbflimsup  25655  itgcn  25834  dvdsq1p  26150  aalioulem2  26321  recosf1o  26521  logrec  26749  xrlimcnp  26954  basellem4  27069  bposlem1  27269  bposlem5  27273  lgsqrmod  27337  lgsdchrval  27339  2lgslem1a1  27374  pntlem3  27594  nosupbnd1  27700  noinfbnd1  27715  oldbday  27915  lrcut  27918  abslts  28263  n0ssoldg  28367  zsoring  28423  bdayfinbndlem1  28481  brbtwn2  28996  axbtwnid  29030  elntg2  29076  umgredgprv  29198  umgrpredgv  29231  usgredgprvALT  29286  fusgrfisstep  29420  fusgrfis  29421  nbupgr  29435  nbumgrvtx  29437  finsumvtxdg2size  29641  wlkp1lem8  29769  upgr2pthnlp  29822  wwlksnextinj  29989  usgr2wspthons3  30057  clwwlkccatlem  30081  clwlkclwwlklem2a1  30084  clwwisshclwws  30107  wwlksext2clwwlk  30149  clwwlknonex2lem2  30200  eucrctshift  30335  eucrct2eupth  30337  numclwwlk2lem1  30468  numclwwlk5lem  30479  frgrreggt1  30485  frgrreg  30486  friendship  30491  blocn2  30901  htthlem  31010  axhcompl-zf  31091  spanuni  31637  spansncol  31661  spansneleq  31663  elspansn5  31667  idcnop  32074  pjnormssi  32261  dmdmd  32393  bian1dOLD  32548  n0nsnel  32607  ifeqeqx  32634  opabssi  32709  ac6mapd  32719  ressupprn  32786  supxrnemnf  32864  rexdiv  33008  xrstos  33093  cnre2csqlem  34106  fsumcvg4  34146  lmxrge0  34148  qqhval2lem  34177  esumpr2  34263  esumcvg  34282  issgon  34319  measxun2  34406  measres  34418  measdivcst  34420  measdivcstALTV  34421  elorrvc  34660  signsply0  34747  bnj580  35110  nummin  35289  axprALT2  35305  0nn0m1nnn0  35356  umgracycusgr  35397  erdsze2lem2  35447  cvmsval  35509  fmlasuc  35629  fundmpss  36010  dfon2lem3  36026  dfrdg4  36194  cgrtriv  36245  btwntriv2  36255  ifscgr  36287  lineext  36319  btwnconn1lem12  36341  colinbtwnle  36361  elicc3  36560  ontgval  36674  onsucconni  36680  axtco1from2  36718  axtcond  36721  axnulregtco  36723  dfttc4lem2  36772  bj-bibibi  36912  bj-cbvalvv  36994  bj-cbval  37001  bj-cbvex  37002  bj-cbvexw  37032  bj-nnf-cbval  37138  bj-equsal  37194  bj-gabeqd  37305  bj-restn0  37463  bj-snmoore  37486  cgsex2gd  37512  bj-elsn0  37530  bj-finsumval0  37660  relowlssretop  37740  sucneqond  37742  finxpsuc  37775  pibt2  37794  wl-nfs1t  37923  finixpnum  37987  ltflcei  37990  matunitlindflem1  37998  poimirlem23  38025  poimirlem24  38026  poimirlem27  38029  poimirlem32  38034  itg2addnclem  38053  areacirclem2  38091  areacirclem5  38094  areacirc  38095  nninfnub  38133  prdstotbnd  38176  heiborlem4  38196  heibor  38203  elghomlem2OLD  38268  grpokerinj  38275  isidlc  38397  disjlem17  39284  prtlem17  39383  dral1-o  39411  axc16g-o  39441  lsator0sp  39508  atlrelat1  39828  cvratlem  39928  diaintclN  41565  dibintclN  41674  cdlemn11pre  41717  dihord2pre  41732  dihintcl  41851  dochkrshp4  41896  lcfrlem9  42057  lcfrlem21  42070  mapdh8e  42291  aks4d1p5  42580  aks6d1c1p1  42607  sticksstones4  42649  0prjspnrel  43092  elrfirn2  43160  rencldnfilem  43280  onsupnmax  43688  onov0suclim  43734  oege1  43766  cantnfresb  43784  dflim5  43789  omabs2  43792  refimssco  44066  rtrclex  44076  intimasn  44116  ss2iundf  44118  ov2ssiunov2  44159  comptiunov2i  44165  iunrelexpuztr  44178  dssmapf1od  44480  mnringmulrcld  44687  mnuprdlem1  44731  mnuprdlem2  44732  snelpwrVD  45289  en3lplem1VD  45301  en3lpVD  45303  orbi1rVD  45306  sbc3orgVD  45309  3impexpVD  45314  equncomVD  45326  trsbcVD  45335  trintALTVD  45338  trintALT  45339  csbingVD  45342  csbsngVD  45351  csbxpgVD  45352  csbrngVD  45354  csbfv12gALTVD  45357  relopabVD  45359  e2ebindVD  45370  xlimpnfxnegmnf  46271  xlimbr  46284  stoweidlem35  46492  stoweidlem48  46505  ormkglobd  47334  cjnpoly  47366  tannpoly  47367  n0nsn2el  47502  rexrsb  47577  2reu8i  47590  funbrafv  47635  rlimdmafv  47654  tz6.12c-afv2  47719  rlimdmafv2  47735  fzopredsuc  47801  2ffzoeq  47805  m1modnep2mod  47835  2timesltsq  47855  eqfvelsetpreimafv  47882  iccpartlt  47913  proththd  48106  even3prm2  48224  fppr2odd  48236  sbgoldbm  48289  nnsum3primesle9  48299  wtgoldbnnsum4prm  48307  bgoldbnnsum3prm  48309  grtrif1o  48447  mgm2mgm  48732  2zrngnmlid  48760  2zrngnmrid  48761  ellcoellss  48940  nneop  49031  fldivexpfllog2  49070  digexp  49112  reorelicc  49215  2itscp  49286  oppc1stflem  49791  prsthinc  49968  elpglem2  50216